aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-30 12:56:06 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-05-30 12:56:06 -0400
commit88160e4186b3a96632806d35472a7d0b05087f47 (patch)
tree1f782f2289565ea76bb62c85f9520bb1970af1a5 /.gitignore
parentfd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff)
Add some test-suite generated files to .gitignore
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore3
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index c55ad24f8..98d974197 100644
--- a/.gitignore
+++ b/.gitignore
@@ -66,9 +66,12 @@ test-suite/coq-makefile/*/Makefile
test-suite/coq-makefile/*/Makefile.conf
test-suite/coq-makefile/*/src
test-suite/coq-makefile/*/theories
+test-suite/coq-makefile/*/theories2
test-suite/coq-makefile/*/html
test-suite/coq-makefile/*/mlihtml
test-suite/coq-makefile/*/subdir/done
+test-suite/coq-makefile/latex1/all.pdf
+test-suite/coq-makefile/merlin1/.merlin
# documentation