X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=9cde82b7535501fb100d9a3a121621fff0d1b301;hb=3e84eec9bbaf93687f72d1a77ca03dea34b50739;hp=ed739eefbebb8c9be4a9e5ab95f919166625a722;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index ed739eefb..9cde82b75 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -206,6 +206,8 @@ class gui () = ~website:"http://helm.cs.unibo.it" () in + connect_menu_item main#contentsMenuItem + (fun () -> ignore (Sys.command "gnome-help ghelp:///home/claudio/miohelm/matita/help/C/matita.xml &")); connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = @@ -1133,7 +1135,7 @@ let interactive_uri_choice let gui = instance () in let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in if (selection_mode <> `SINGLE) && - (Helm_registry.get_bool "matita.auto_disambiguation") + (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") then Lazy.force nonvars_uris else begin