aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-12 10:50:48 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-12 17:18:07 +0200
commitd4c9a7c5b47670bad12d54a3fd4de0ad4eceb1ee (patch)
treea5010aed6f4b186beb866110ec21d429dfc4c002 /.gitignore
parent8b76e2ecdd355e0088fd0542d5acd492a6a89ec2 (diff)
downloadcompcert-kvx-d4c9a7c5b47670bad12d54a3fd4de0ad4eceb1ee.tar.gz
compcert-kvx-d4c9a7c5b47670bad12d54a3fd4de0ad4eceb1ee.zip
We can ignore the generated automation. Bug 17392
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 1c8ff7d9..fc387e39 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,6 +37,7 @@ cparser/Parser.v
cparser/Lexer.ml
cparser/pre_parser.ml
cparser/pre_parser.mli
+cparser/pre_parser.automaton
lib/Readconfig.ml
lib/Tokenize.ml
driver/Version.ml