diff options
| author | Hugo Herbelin | 2020-04-22 22:37:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-22 22:37:13 +0200 |
| commit | 99dc43029b743412be3ad8b597a38bdd135e2e9c (patch) | |
| tree | 389a23824d39c350b7319d43a73dd4f3172f3453 /dev/include | |
| parent | 7e2167f5bfd7d70847d1b1ece34c1f0303f46fc8 (diff) | |
CoqIDE: Avoid invalidation of an iterator in insert callback.
This hopefully fix the segfaults we observe with completion.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions