From: Claudio Sacerdoti Coen Date: Wed, 26 Dec 2018 18:40:44 +0000 (+0100) Subject: useful comment X-Git-Tag: make_still_working~229^2~1^2~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa21e88e6e9464dbd2f76d8b1d6094054a6ec19c;p=helm.git useful comment --- diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index c1e8e9fc5..4dc6274a3 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -97,6 +97,8 @@ let interactive_uri_choice | uris -> return (Some (List.map NReference.reference_of_string uris))); connect_button dialog#uriChoiceAbortButton (fun _ -> return None); dialog#uriChoiceDialog#show (); + (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling + other dialogs *) GtkThread.main (); (match !choices with | None -> raise MatitaTypes.Cancel