aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Roux2019-11-13 17:24:38 +0100
committerPierre Roux2019-11-13 17:25:58 +0100
commitdbffbe71bd0437ff069b1c13720d7400170959a9 (patch)
tree8d359f6ff03997bce1a6e941aed45ab43f006e4d
parentb9def53df5a69d5d4dbf46bd846281220b4fe1db (diff)
Update .gitignore after #11092
-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