diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fd460c4e97..86045ee19a 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -279,11 +279,12 @@ let run_command f c = let browse f url = let com = Minilib.subst_command_placeholder !current.cmd_browse url in - let s = Sys.command com in + let _ = Unix.open_process_out com in () +(* This beautiful message will wait for twt ... if s = 127 then f ("Could not execute\n\""^com^ "\"\ncheck your preferences for setting a valid browser command\n") - +*) let doc_url () = if !current.doc_url = use_default_doc_url || !current.doc_url = "" then let addr = List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";"index.html"] in |