summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorJonathan Protzenko2023-01-25 13:12:01 -0800
committerSon HO2023-06-04 21:44:33 +0200
commite1ee59f6a45482e93901f6a549f594fd6ef15234 (patch)
treec9d20fdc675823b058b7d364852c6a5d0bfaf729 /.gitignore
parentdee74ca1f90acb076289286f6f69df65e63604ce (diff)
New directory structure and corresponding extraction, + misc fixes, for Lean
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index d0a4be47..e8b8b7a4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -67,3 +67,4 @@ nohup.out
*.txt
*/.#*
*.smt2
+.DS_Store