diff options
| author | Guillaume Melquiond | 2016-09-28 17:00:09 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-10-22 11:57:58 +0200 |
| commit | cc2778c3310a75585c00f0eb659ddde7aee2944a (patch) | |
| tree | 8a0a403eb33401748a6c0d4c67465661270e8729 /kernel/cbytecodes.ml | |
| parent | 9f8714f4cd3fb59ce38afee48caf081db1919c0c (diff) | |
Do not stop propagation of signals when Coq is busy (bug #3941).
When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions