From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 22 Nov 2008 16:48:15 +0000 (+0000)
Subject: if gnome-help is not installed, prints an error message
X-Git-Tag: make_still_working~4516
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=0a54b76b4322ba0a490af843c4436271c0014a83;p=helm.git

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 ac34052c1..0cbf2d89a 100644
--- 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 () =