aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore8
1 files changed, 8 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 371136fc7..8bbfce5d8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -60,6 +60,14 @@ test-suite/.nra.cache
test-suite/trace
test-suite/misc/universes/all_stdlib.v
test-suite/misc/universes/universes.txt
+test-suite/coq-makefile/*/actual
+test-suite/coq-makefile/*/desired
+test-suite/coq-makefile/*/Makefile
+test-suite/coq-makefile/*/Makefile.conf
+test-suite/coq-makefile/*/src/test.ml
+test-suite/coq-makefile/*/html
+test-suite/coq-makefile/*/mlihtml
+test-suite/coq-makefile/*/subdir/done
# documentation