commit by user mkmluser

[helm.git] / weblib / commit_test2.ma

diff --git a/weblib/commit_test2.ma b/weblib/commit_test2.ma
index 6745f532a52d9603b1d8beb542f7fa4411bd87cf..51bd8abb100ee5d9daab7a1646573ae7882d6b32 100644 (file)
--- a/weblib/commit_test2.ma
+++ b/weblib/commit_test2.ma
@@ -1 +1,3 @@
-axiom pluto : Prop.
+(* test2 *)
+
+axiom pluto : Prop.
\ No newline at end of file