implements a better way to respect the Unix convention that processes receive their own name

as first argument.  This is needed to make external tactics work when the external program
is interpreted and the operating system is Mac OS

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10437 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 31e8f5649e..c5ed94d5c1 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -215,7 +215,7 @@ let connect writefun readfun com =
   let pid = 
     let ch_to' = Unix.descr_of_in_channel ch_to_in in
     let ch_from' = Unix.descr_of_out_channel ch_from_out in
-    try Unix.create_process com [||] ch_to' ch_from' Unix.stdout
+    try Unix.create_process com [|com|] ch_to' ch_from' Unix.stdout
     with Unix.Unix_error (err,_,_) ->
       close_in ch_to_in; close_in ch_from_in; close_out ch_from_out;
       unlink tmp_from; unlink tmp_to;