aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-08-18 16:18:23 +0200
committerJosh Chen2018-08-18 16:18:23 +0200
commit03c734ea067bd28210530d862137133e2215ca80 (patch)
tree3e21b040d84af0337abecd7d6db2a530764c144b
parenta1603ffdddcbe333a3e4f0f328a4c25698c2d475 (diff)
HoTT_Test.thy should go in test/
-rw-r--r--tests/Test.thy (renamed from HoTT_Test.thy)2
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT_Test.thy b/tests/Test.thy
index da044b4..433039c 100644
--- a/HoTT_Test.thy
+++ b/tests/Test.thy
@@ -1,4 +1,4 @@
-(* Title: HoTT/HoTT_Test.thy
+(* Title: HoTT/tests/Test.thy
Author: Josh Chen
Date: Aug 2018