From 74bd95d10b9f4cccb4bd5b855786c444492b201b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 21 Jan 2014 20:12:58 +0100
Subject: Relaunch all Unix.waitpid when they ended with EINTR

 Moreover, cleanup of System.connect (used by the "external" tactic).
---
 plugins/micromega/mutils.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 0b98696c95..ae89364e62 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -403,6 +403,12 @@ end
 
 module TagSet = Set.Make(Tag)
 
+(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *)
+
+let rec waitpid_non_intr pid =
+  try snd (Unix.waitpid [] pid)
+  with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid
+
 (**
   * Forking routine, plumbing the appropriate pipes where needed.
   *)
@@ -422,7 +428,7 @@ let command exe_path args vl =
     flush outch ;
 
   (* Wait for its completion *)
-    let _pid,status = Unix.waitpid [] pid in
+    let status = waitpid_non_intr pid in
 
       finally
         (* Recover the result *)
-- 
cgit v1.2.3