diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-04 16:23:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:50:05 +0200 |
| commit | 62807372f1e3f78dffc02c07b0b801d4d8f4a78f (patch) | |
| tree | a35e78799a84c31e644884bb43e49a4724d2adbd /ide/coq.ml | |
| parent | 7dba9d3f3ce62246b9d8562d2818c63ba37b206e (diff) | |
Coqide: check_connection now also checks correct loading of coqide plugin +
reports errors also from stderr.
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index e8e925e44..aba463488 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -151,12 +151,12 @@ let print_status = function let check_connection args = let lines = ref [] in let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in let cmd = requote cmd in try - let ic = Unix.open_process_in cmd in - lines := read_all_lines ic; - match Unix.close_process_in ic with + let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in + lines := read_all_lines oc @ read_all_lines ec; + match Unix.close_process_full (oc,ic,ec) with | Unix.WEXITED 0 -> () (* coqtop seems ok *) | st -> raise (WrongExitStatus (print_status st)) with e -> connection_error cmd !lines e |