From 6ed4f78cdb661e9d7509913f142275e384122d48 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 4 Feb 2005 22:50:51 +0000
Subject: Bug synchronisation fonction connect

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6685 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/system.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/system.ml b/lib/system.ml
index 237c9848fd..241477e8c4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -196,18 +196,16 @@ let connect writefun readfun com =
     with Sys_error s ->
       close_out ch_to_out; close_in ch_to_in; 
       error ("Cannot set connection from "^com^"("^s^")") in
+  writefun ch_to_out;
+  close_out ch_to_out;
   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
     with Unix.Unix_error (err,_,_) ->
-      close_in ch_to_in;
-      close_out ch_to_out;
-      close_in ch_from_in;
-      close_out ch_from_out;
+      close_in ch_to_in; close_in ch_from_in; close_out ch_from_out;
+      unlink tmp_from; unlink tmp_to;
       error ("Cannot execute "^com^"("^(Unix.error_message err)^")") in
-  writefun ch_to_out;
-  close_out ch_to_out;
   close_in ch_to_in;
   close_out ch_from_out;
   (match snd (Unix.waitpid [] pid) with
-- 
cgit v1.2.3