aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore8
1 files changed, 7 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index 02379a3b..9e530127 100644
--- a/.gitignore
+++ b/.gitignore
@@ -28,12 +28,18 @@ Makefile.config
compcert.ini
ia32/ConstpropOp.v
ia32/SelectOp.v
+ia32/SelectLong.v
powerpc/ConstpropOp.v
powerpc/SelectOp.v
+powerpc/SelectLong.v
arm/ConstpropOp.v
arm/SelectOp.v
+arm/SelectLong.v
+x86_64/ConstpropOp.v
+x86_64/SelectOp.v
+x86_64/SelectLong.v
backend/SelectDiv.v
-backend/SelectLong.v
+backend/SplitLong.v
backend/CMlexer.ml
backend/CMparser.ml
backend/CMparser.mli