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#