aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-18 17:54:48 +0100
committerEmilio Jesus Gallego Arias2019-11-18 17:54:48 +0100
commit4aa756934eb37c6b6d70eddf2b46871bb8ff0956 (patch)
tree59cb6d1ec3edd97d5b6b90d7c451e8c22e2419d6
parent64265294b519d7cd9f982edf24991c7f210933a9 (diff)
parentdbffbe71bd0437ff069b1c13720d7400170959a9 (diff)
Merge PR #11115: [dune] Update .gitignore after #11092
Reviewed-by: ejgallego
-rw-r--r--.gitignore2
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index a1c0dc774e..6c117028a9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,6 +55,7 @@ _build
config/Makefile
config/coq_config.ml
config/coq_config.py
+config/dune.c_flags
config/Info-*.plist
dev/ocamldebug-coq
plugins/micromega/csdpcert
@@ -152,7 +153,6 @@ plugins/ssr/ssrvernac.ml
# other auto-generated files
-kernel/byterun/dune.c_flags
kernel/byterun/coq_instruct.h
kernel/byterun/coq_jumptbl.h
kernel/genOpcodeFiles.exe