diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index b79e4b9361..f4fd73d6fd 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -268,9 +268,11 @@ let run_command f c = (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) let browse f url = - let l,r = !current.cmd_browse in - let (_s,_res) = run_command f (l ^ url ^ r) in - () + let com = Flags.subst_command_placeholder !current.cmd_browse url in + let (s,_res) = run_command f com in + if s = Unix.WEXITED 127 then + prerr_endline + ("Could not execute\n \""^com^"\"\ncheck your preferences for setting a valid browser command") let url_for_keyword = let ht = Hashtbl.create 97 in @@ -295,7 +297,8 @@ let url_for_keyword = let browse_keyword f text = try let u = url_for_keyword text in browse f (!current.doc_url ^ u) - with _ -> () + with Not_found -> + prerr_endline ("No documentation found for "^text) let underscore = Glib.Utf8.to_unichar "_" (ref 0) |