From 3ab7a14bb005dae4141b434c1dd8ac73b4af2aa1 Mon Sep 17 00:00:00 2001
From: bertot
Date: Fri, 11 Jan 2008 14:50:44 +0000
Subject: 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
---
 lib/system.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

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;
-- 
cgit v1.2.3