aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index e96978b4c..79cdd99f7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -90,7 +90,6 @@ plugins/dp/dp_zenon.ml
tools/gallina_lexer.ml
tools/coqwc.ml
tools/coqdep_lexer.ml
-tools/coqdoc/index.ml
tools/coqdoc/cpretty.ml
# .mly files