aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore11
1 files changed, 9 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore
index 242dbddb..eaa8caf3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,10 +19,10 @@ cchecklink.byte
clightgen
clightgen.byte
tools/ndfun
+tools/modorder
Makefile.config
-# ocamlbuild's temp dir
-_build/
# Generated files
+.depend.extr
compcert.ini
ia32/ConstpropOp.v
ia32/SelectOp.v
@@ -32,6 +32,13 @@ arm/ConstpropOp.v
arm/SelectOp.v
backend/SelectDiv.v
backend/SelectLong.v
+backend/CMlexer.ml
+backend/CMparser.ml
+backend/CMparser.mli
+cparser/Lexer.ml
+cparser/pre_parser.ml
+cparser/pre_parser.mli
+lib/Tokenize.ml
# Documentation
doc/coq2html
doc/coq2html.ml