aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorJosh Chen2020-04-02 17:57:48 +0200
committerJosh Chen2020-04-02 17:57:48 +0200
commitc2dfffffb7586662c67e44a2d255a1a97ab0398b (patch)
treeed949f5ab7dc64541c838694b502555a275b0995 /.gitignore
parentb01b8ee0f3472cb728f09463d0620ac8b8066bcb (diff)
Brand-spanking new version using Spartan infrastructure
Diffstat (limited to '')
-rw-r--r--.gitignore13
1 files changed, 2 insertions, 11 deletions
diff --git a/.gitignore b/.gitignore
index e863a1e..160465a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,12 +1,3 @@
-.directory
-*.thy~
+*~
\#*.thy#
-
-ex/*.thy~
-ex/\#*.thy#
-
-ex/Hott book/*.thy~
-ex/Hott book/\#*.thy#
-
-tests/*.thy~
-tests/\#*.thy#
+\#*.ML#