aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-23 17:18:39 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:27 +0200
commite9156da20ec5332b1b53a6c44127e0f822891d16 (patch)
tree87574e62f236faa8c0c00393d78b1e5233cfe490 /.gitignore
parentcd8f10fe54c956f1e797da3d165c3b29ffee615b (diff)
test suite for coq_makefile
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