From f560d8b91b92cb537e415d622d4f5f248c18dde0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Mar 2020 18:28:21 +0100
Subject: Prevent CoqIDE from hanging when invalid channels are still open.

This behaviour happens as a sub-bug of #10169 for instance.
---
 ide/coqide.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 61e95c21b1..553b834a37 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -244,6 +244,13 @@ let close_and_quit () =
   List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages;
   exit 0
 
+(* Work around a deadlock due to OCaml exit cleanup. The standard [exit]
+   function calls [flush_all], which can block if one of the opened channels is
+   not valid anymore. We do not register [at_exit] functions in CoqIDE, so
+   instead of flushing we simply die as gracefully as possible in the function
+   below. *)
+external sys_exit : int -> 'a = "caml_sys_exit"
+
 let crash_save exitcode =
   Minilib.log "Starting emergency save of buffers in .crashcoqide files";
   let idx =
@@ -263,7 +270,7 @@ let crash_save exitcode =
   in
   List.iter save_session notebook#pages;
   Minilib.log "End emergency save";
-  exit exitcode
+  sys_exit exitcode
 
 end
 
-- 
cgit v1.2.3