aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-07-27 14:31:09 +0200
committerJosh Chen2020-07-27 14:31:09 +0200
commit2a78ddc733340a72351df09a12ce4fc695b93de7 (patch)
tree4946b6478b67500c847272f8e6be20aae1be81ae
parent184b1d493be87fd96057402c67ad4382cb60a145 (diff)
update .gitignore
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index fb8160e..82f42f5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,4 @@
*~
\#*.thy#
\#*.ML#
-Test.thy