aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore3
1 files changed, 1 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore
index 116f88dd7..1cbf56e3c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -44,7 +44,6 @@ TAGS
.pc
bin/
_build
-plugins/*/*_mod.ml
myocamlbuild_config.ml
config/Makefile
config/coq_config.ml
@@ -114,7 +113,7 @@ tools/ocamllibdep.ml
tools/coqdoc/cpretty.ml
ide/xml_lexer.ml
-# .ml4 files
+# .ml4 / .mlp files
g_*.ml