aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-07-25 12:02:32 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-07-25 12:08:08 +0200
commitbac2bf05c2586c447b43436af73a1a279ecd7035 (patch)
treee8f5426a8ecd5c09f94246ece7d1ab802b6357a2 /.gitignore
parente9d480b0bea05debefe3f52e5881ea7e00cef809 (diff)
Add lia.cache to the .gitignore
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 7a8b9e625..1a98af1f2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -148,6 +148,7 @@ kernel/copcodes.ml
tools/tolink.ml
theories/Numbers/Natural/BigN/NMake_gen.v
ide/index_urls.txt
+lia.cache
# mlis documentation