From 45e43916a7ce756b617b7ba3f8062f7956872fb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 17:10:16 +0100 Subject: Tentative fix for bug #4614: "Fully check the document" is uninterruptable. The SIGINT sent to the master coqtop process was lost in a watchdog thread, so that the STM resulted in an inconsistent state. This patch catches gracefully the exception and kills the task as if it were normally cancelled. Note that it probably won't work on non-POSIX architectures, but it does not really matter because interrupt was already badly handled anyway. --- stm/asyncTaskQueue.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 5f018ec39..8649a14c5 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -184,6 +184,13 @@ module Make(T : Task) = struct let () = Unix.sleep 1 in kill_if () in + let kill_if () = + try kill_if () + with Sys.Break -> + let () = stop_waiting := true in + let () = TQueue.broadcast queue in + Worker.kill proc + in let _ = Thread.create kill_if () in try while true do -- cgit v1.2.3