From 0a54b76b4322ba0a490af843c4436271c0014a83 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 22 Nov 2008 16:48:15 +0000 Subject: [PATCH] if gnome-help is not installed, prints an error message --- helm/software/matita/matitaGui.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) 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 () = -- 2.39.2