diff options
| author | Pierre-Marie Pédrot | 2016-03-15 17:10:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-15 18:12:58 +0100 |
| commit | 45e43916a7ce756b617b7ba3f8062f7956872fb3 (patch) | |
| tree | a9f07de2eccc00fe0e52c904a8f6ea571eb82736 /dev/header | |
| parent | 8f5ca2a6100eb243d2a9842a13e02b793ee0aea1 (diff) | |
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.
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions