summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore4
1 files changed, 0 insertions, 4 deletions
diff --git a/.gitignore b/.gitignore
index 5b4c029..fee7bae 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,7 +11,3 @@
*.byte
setup.log
setup.data
-setup.ml
-myocamlbuild.ml
-Makefile
-configure