aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-12-17 11:25:03 +0100
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-12-17 11:25:03 +0100
commitadff86c007196e4389668c7935b7891c5b4217c7 (patch)
tree32954898ed941f92069092fa9c56d1a5c14e9fef /.gitignore
parent471a8363c185e073fdfb8aefeb863b215870285d (diff)
downloadcompcert-kvx-adff86c007196e4389668c7935b7891c5b4217c7.tar.gz
compcert-kvx-adff86c007196e4389668c7935b7891c5b4217c7.zip
fix extraction of non-aarch64 targets
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 1d6cad94..fa9b1c67 100644
--- a/.gitignore
+++ b/.gitignore
@@ -76,6 +76,7 @@
/lib/Responsefile.ml
/driver/Version.ml
/driver/Compiler.v
+/extraction/extraction.v
# Documentation
/doc/coq2html
/doc/coq2html.ml