aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 2e5529ccfb..c30fd850a1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -147,6 +147,7 @@ plugins/ssr/ssrvernac.ml
kernel/byterun/coq_jumptbl.h
kernel/copcodes.ml
+kernel/uint63.ml
ide/index_urls.txt
.lia.cache
.nia.cache