aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-07-25 12:05:00 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-07-25 12:08:08 +0200
commit933ec4bdb6a9a66b7556797aa8804858aa591b54 (patch)
treef22732bfa4677eb1f16ad7f3a3177410bf169112 /.gitignore
parentbac2bf05c2586c447b43436af73a1a279ecd7035 (diff)
Add *.crashcoqide files to the .gitignore.
They occasionally show up while testing. I think it cleaner to ignore them.
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore3
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 1a98af1f2..1ea6d6e12 100644
--- a/.gitignore
+++ b/.gitignore
@@ -156,3 +156,6 @@ dev/ocamldoc/html/
dev/ocamldoc/coq.*
dev/ocamldoc/ocamldoc.sty
dev/myinclude
+
+# coqide generated files (when testing)
+*.crashcoqide \ No newline at end of file