From ad513f2343d3cced4050b95803b33b28dd2382f8 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 3 Oct 2013 09:09:22 +0000
Subject: STM: avoid "kill 9 pid" if we know the slave died

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16838 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 8165da5d52..51fa14ea46 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -666,7 +666,6 @@ end = struct (* {{{ *)
       Unix.close s2c_w;
       let s =
         Unix.in_channel_of_descr s2c_r, Unix.out_channel_of_descr c2s_w, pid in
-      at_exit(fun () -> try Unix.kill pid 9 with Unix.Unix_error _ -> ());
       s
 
     let init manage_slave =
@@ -789,6 +788,9 @@ end = struct (* {{{ *)
 
   let rec manage_slave respawn =
     let ic, oc, pid = respawn () in
+    let kill_pid =
+      ref (fun () -> try Unix.kill pid 9 with Unix.Unix_error _ -> ()) in
+    at_exit (fun () -> !kill_pid ());
     let last_task = ref None in
     try
       while true do
@@ -838,6 +840,7 @@ end = struct (* {{{ *)
             (* XXX do something sensible *)
       done
     with Sys_error _ | Invalid_argument _ | End_of_file ->
+      kill_pid := (fun () -> ());
       msg_warning(strbrk "The slave process died badly.");
       (match !last_task with
       | Some task ->
-- 
cgit v1.2.3