diff options
| author | bertot | 2008-01-11 14:50:44 +0000 |
|---|---|---|
| committer | bertot | 2008-01-11 14:50:44 +0000 |
| commit | 3ab7a14bb005dae4141b434c1dd8ac73b4af2aa1 (patch) | |
| tree | 22283599628b301b7da2f29ee905db308e43dea0 /lib/system.ml | |
| parent | e685bc6f1bc8f7e1160cef53127a11d8d7be7306 (diff) | |
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
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 2 |
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; |