]> matita.cs.unibo.it Git - helm.git/commitdiff
Fix dialog win
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 21 Dec 2018 20:47:51 +0000 (21:47 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 21 Dec 2018 20:47:51 +0000 (21:47 +0100)
It used to be destroyed when closed the first time

matita/matita/matitaGui.ml

index d8de328ef17d5dad8ea13e94ec6aa2349075c21c..b294af25d45a5ed7c46a1e0dd991a317c39c82c8 100644 (file)
@@ -461,6 +461,7 @@ class gui () =
         ~website:"http://matita.cs.unibo.it"
         ()
       in
+      ignore(about_dialog#event#connect#delete (fun _ -> true));
       ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ()));
       connect_menu_item main#contentsMenuItem (fun () ->
         if 0 = Sys.command "which gnome-help" then