aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorVincent Laporte2019-03-26 14:28:07 +0000
committerVincent Laporte2019-03-26 14:28:07 +0000
commit8ad84a3541bee26d1ba0644274dcf4d9e287c124 (patch)
treed23d3cdc1b80268449a69023f4bc3120ee39c416 /.gitignore
parenta59d80d3d482813b3c3c1ebce18ae39c3d09e5be (diff)
Ignore generated files for CoqIDE bindings
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore2
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 4e02e7617c..23e305892e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -150,6 +150,8 @@ kernel/byterun/coq_jumptbl.h
kernel/genOpcodeFiles.exe
kernel/copcodes.ml
kernel/uint63.ml
+ide/default.bindings
+ide/default_bindings_src.exe
ide/index_urls.txt
.lia.cache
.nia.cache