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 /plugins | |
| parent | dbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff) | |
Prevent CoqIDE from hanging when invalid channels are still open.
This behaviour happens as a sub-bug of #10169 for instance.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions