From: Claudio Sacerdoti Coen Date: Fri, 21 Dec 2018 20:47:51 +0000 (+0100) Subject: Fix dialog win X-Git-Tag: make_still_working~229^2~1^2~34 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=881672563cb65777d23c9dbe2c24de5214c82eb3;p=helm.git Fix dialog win It used to be destroyed when closed the first time --- diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index d8de328ef..b294af25d 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -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