diff options
| author | Pierre-Marie Pédrot | 2020-03-09 18:28:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-09 18:29:28 +0100 |
| commit | f560d8b91b92cb537e415d622d4f5f248c18dde0 (patch) | |
| tree | 4b613df2dda8a57ce2d17cb0520e8f609d05face | |
| parent | dbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff) | |
Prevent CoqIDE from hanging when invalid channels are still open.
This behaviour happens as a sub-bug of #10169 for instance.
| -rw-r--r-- | ide/coqide.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |