aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index bdd692420f..aab1d1ede7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -155,6 +155,7 @@ kernel/byterun/coq_jumptbl.h
kernel/genOpcodeFiles.exe
kernel/vmopcodes.ml
kernel/uint63.ml
+kernel/float64.ml
ide/coqide/default.bindings
ide/coqide/default_bindings_src.exe
ide/coqide/index_urls.txt