aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index e52091ee2..db12a9de2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -150,7 +150,6 @@ plugins/ssr/ssrvernac.ml
kernel/byterun/coq_jumptbl.h
kernel/copcodes.ml
tools/tolink.ml
-theories/Numbers/Natural/BigN/NMake_gen.v
ide/index_urls.txt
.lia.cache
checker/names.ml