aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore4
1 files changed, 0 insertions, 4 deletions
diff --git a/.gitignore b/.gitignore
index fd993627..1d1ff9df 100644
--- a/.gitignore
+++ b/.gitignore
@@ -38,9 +38,6 @@ arm/SelectOp.v
arm/SelectLong.v
backend/SelectDiv.v
backend/SplitLong.v
-backend/CMlexer.ml
-backend/CMparser.ml
-backend/CMparser.mli
cparser/Parser.v
cparser/Lexer.ml
cparser/pre_parser.ml
@@ -53,7 +50,6 @@ cparser/handcrafted.messages.raw
cparser/deLexer
cparser/tests/generated/*.c
cparser/tests/generated/*.err
-backend/CMparser.automaton
lib/Readconfig.ml
lib/Tokenize.ml
lib/Responsefile.ml