aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-07-10 01:34:18 -0700
committerGravatar Jason Gross <jgross@mit.edu>2016-07-10 01:34:18 -0700
commit8703b2bc7a31807357a300bc017d13ba596575f9 (patch)
tree5ef7324cefbc000cbdb476b2f4343dd14f12b478 /.gitignore
parent649d3e8730703d47068418c312f33550b8709695 (diff)
Update .gitignore
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index b8cf1d4bc..b22a815ee 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,6 +8,7 @@
.#*
Makefile.bak
Makefile.coq
+Makefile.coq.bak
csdp.cache
lia.cache
nlia.cache