diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 00:16:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 00:23:00 +0200 |
| commit | 47098e8619f269ddaaf621936ae90b9dfa128871 (patch) | |
| tree | 9f538f6801e506d7eea5d01d3b80d1396a47e808 /pretyping | |
| parent | 4b4397e185cee54052819ad63bef3ecd56ba4512 (diff) | |
Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.
Instead of relaunching the coqtop process and then open the warning window,
we rather fire the warning and wait for the user to press the OK button before
doing anything.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions