diff options
| author | Michael Soegtrop | 2020-03-10 21:19:37 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2020-03-10 21:19:37 +0100 |
| commit | 4cc3f613c96197dd9e6b5f531fa4c68968f27176 (patch) | |
| tree | afa3990aa5fc44c5367e47c813a8022365ef8cd2 /dev/include | |
| parent | 3a5469b2097c55ecf952ead470caf03b6112cd9e (diff) | |
| parent | f560d8b91b92cb537e415d622d4f5f248c18dde0 (diff) | |
Merge PR #11788: Prevent CoqIDE from hanging when invalid channels are still open.
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions