if gnome-help is not installed, prints an error message

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index ac34052c134d5e3da486aa18c29ca8e5fde8c20e..0cbf2d89ada81b5287a9bc4bba440315410e8146 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -433,10 +433,18 @@ class gui () =
       in
       ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ()));
       connect_menu_item main#contentsMenuItem (fun () ->
-        let cmd =
-          sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
-        in
-        ignore (Sys.command cmd));
+        if 0 = Sys.command "which gnome-help" then
+          let cmd =
+            sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
+          in
+           ignore (Sys.command cmd)
+        else
+          MatitaGtkMisc.report_error ~title:"help system error"
+           ~message:(
+              "The program gnome-help is not installed\n\n"^
+              "To browse the user manal it is necessary to install "^
+              "the gnome help syste (also known as yelp)") 
+           ~parent:main#toplevel ());
       connect_menu_item main#aboutMenuItem about_dialog#present;
         (* findRepl win *)
       let show_find_Repl () =