From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 21 Jul 2005 11:10:30 +0000 (+0000)
Subject: Comment "comments" removed from the outbox :-)
X-Git-Tag: V_0_7_2~132
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d096ec7c396dce8d9bbd71bdee946103d1dd8890;p=helm.git

Comment "comments" removed from the outbox :-)
---

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 8d8249765..3e8fde7a9 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -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*)