aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-24 13:09:06 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-04-24 13:09:06 -0400
commitf0e6e8559ab4950e3629f771ed2eaa166636dcd6 (patch)
tree19b36c1429105ffa73705cd0c693b4146657ed25 /.gitignore
parent74d9b4dd9e50be882571e7344885fc0365fe674a (diff)
Track .dir-locals.el rather than generating it
Since we're only using one version of coqprime, we no longer need to generate .dir-locals.el
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index db3634707..8547a7612 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,7 +6,6 @@
*.vo
*~
.#*
-/.dir-locals.el
Makefile.bak
Makefile.coq
Makefile.coq.bak