aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-29 14:54:06 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-29 14:54:06 +0200
commit5cf814404cec9a8702e4bfa88e0f9176fa04ecfb (patch)
treefabd44046e3e5b9aaac7f33b9e4dddaa8d3f06e8 /.gitignore
parent3208e22ea89c459a5a7944ad8e82511d4a5328fa (diff)
parent477f73ef96d957de5a896a05175ceaab7e0dce03 (diff)
downloadcompcert-5cf814404cec9a8702e4bfa88e0f9176fa04ecfb.tar.gz
compcert-5cf814404cec9a8702e4bfa88e0f9176fa04ecfb.zip
Merge branch 'master' into advanced-diagnostics
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 9a85f487..02379a3b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,6 +52,7 @@ cparser/tests/generated/*.err
backend/CMparser.automaton
lib/Readconfig.ml
lib/Tokenize.ml
+lib/Responsefile.ml
driver/Version.ml
# Documentation
doc/coq2html