aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-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#