aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-12 12:57:19 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-12 12:57:19 -0400
commit4e13647d8f7a46945443e016ea3f248040be8a06 (patch)
treee1bceefb791f74c8c0af81ea4b372b9872ca7a63 /.gitignore
parent51cd9ee4b579ca38a221011de568f275b9dfb7c6 (diff)
Better support for coq_makefile2 with fewer warnings
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 8547a7612..ef8de5c6c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,7 @@
Makefile.bak
Makefile.coq
Makefile.coq.bak
+Makefile-old.conf
csdp.cache
lia.cache
nlia.cache