aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tools/coqc.ml18
1 files changed, 17 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5aa6f0b049..80733e668d 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -18,6 +18,10 @@
line to a process running "coqtop -batch -compile <file>".
*)
+(* Environment *)
+
+let environment = Unix.environment ()
+
let binary = ref "coqtop"
let image = ref ""
@@ -38,7 +42,19 @@ let rec make_compilation_args = function
let compile command args files =
let args' = command :: args @ (make_compilation_args files) in
- Unix.execvp command (Array.of_list args')
+ match Sys.os_type with
+ | "Win32" ->
+ let pid =
+ Unix.create_process_env command (Array.of_list args') environment
+ Unix.stdin Unix.stdout Unix.stderr
+ in
+ let status = snd (Unix.waitpid [] pid) in
+ let errcode =
+ match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c
+ in
+ exit errcode
+ | _ ->
+ Unix.execvpe command (Array.of_list args') environment
let usage () =
Usage.print_usage_coqc () ;