From df95bf41c5d60d5baa915cb3ca6080af4da968ec Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 21 Apr 2011 22:44:22 +0000
Subject: Coqide: let's try to be synchronuous when killing coqtop

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

diff --git a/ide/coq.ml b/ide/coq.ml
index dda040e296..ef444292d6 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -178,7 +178,8 @@ let break_coqtop coqtop =
 
 let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
 
-let blocking_kill pid =
+let kill_coqtop coqtop =
+  let pid = coqtop.pid in
   begin
     try !killer pid
     with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
@@ -188,9 +189,6 @@ let blocking_kill pid =
     Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
   with _ -> prerr_endline "Error while waiting for child"
 
-let kill_coqtop coqtop =
-  ignore (Thread.create blocking_kill coqtop.pid)
-
 (** * Calls to coqtop *)
 
 (** Cf [Ide_intf] for more details *)
-- 
cgit v1.2.3