diff options
| author | Emilio Jesus Gallego Arias | 2017-09-24 15:58:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-09-29 11:47:03 +0200 |
| commit | d14215865ec702897fd22a8d9272fede00cda11f (patch) | |
| tree | 04b824e1fd17f042e1f3aacb83a4b06f5e2f1ab6 /dev | |
| parent | 06a723190858da8ed3f30736f22398aa7822c959 (diff) | |
[ide] Avoid duplicate error printing (BZ#5583)
See the discussion in the bug tracker, basically the STM delays the
feedback error message to a point where CoqIDE has forgotten about the
sentence, thus we were processing such errors in the generic case,
printing them twice as the Fail case will also do it.
We could indeed revert back to the 8.6 strategy for error (print
always from Fail and ignore Feedback), however I feel that time will
be better spent by fixing the STM than adding more CoqIDE workarounds.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions