From d3fb99846bdb9f7e0724dde70c8704dfda843bbb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Sep 2014 16:42:53 +0200 Subject: Revert "coqc: execvp is now available even on win32" This reverts commit 60c390951cb2d771c16758a84bf592d06769da14. The reason is that execvp exists on windows but is "non blocking". So coqc would detach "coqtop -compile" and make would fail trying to step to the next target before "coqtop -compile" terminates (because coqc did terminate already). --- tools/coqc.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) 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 ". *) +(* 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 () ; -- cgit v1.2.3