aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-19 16:24:28 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-19 16:24:28 +0100
commite51ffb6c1d9411515facc5e97a4e8dba5d8b55ab (patch)
tree80a7fc8212d28712365082e1a2a2d0fa28cedad3 /.gitignore
parentc130f4936bad11fd6dab3a5d142b870d2a5f650c (diff)
parentb0eb1dfc9fd7b15c556c49101390d882b0f00f8a (diff)
downloadcompcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.tar.gz
compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.zip
Merge branch 'master' into no-shell
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index eaa8caf3..72fb793b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -35,6 +35,7 @@ backend/SelectLong.v
backend/CMlexer.ml
backend/CMparser.ml
backend/CMparser.mli
+cparser/Parser.v
cparser/Lexer.ml
cparser/pre_parser.ml
cparser/pre_parser.mli