aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-11-22 14:21:19 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-11-22 14:21:19 +0100
commitcf646d855395a9d0c40613098debbbd895c4eef8 (patch)
tree1210165fb6472623dbabc6e5afe365fdd38ad205 /.gitignore
parent6fb31c8a00e67f5a91983fe92f6df95d5f54a0c1 (diff)
downloadcompcert-kvx-cf646d855395a9d0c40613098debbbd895c4eef8.tar.gz
compcert-kvx-cf646d855395a9d0c40613098debbbd895c4eef8.zip
Replace ocamlbuild by a second-stage makefile to compile the OCaml code and produce the executables.
configure: add check for GNU make.
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