]> matita.cs.unibo.it Git - helm.git/commitdiff
Comment "comments" removed from the outbox :-)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 11:10:30 +0000 (11:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 11:10:30 +0000 (11:10 +0000)
helm/matita/matitaGui.ml

index 8d82497654a94546595fab91019846957ca43a5b..3e8fde7a9fc03d3586c7fa6413bde7ff52828408 100644 (file)
@@ -168,7 +168,7 @@ class gui () =
       let about_dialog =
        GWindow.about_dialog
         ~authors:(parse_txt_file "AUTHORS")
-        ~comments:"comments"
+        (*~comments:"comments"*)
         ~copyright:"Copyright (C) 2005, the HELM team"
         ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
         (*?logo:GdkPixbuf.pixbuf*)