commit by user mkmluser

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