diff options
| author | Hugo Herbelin | 2020-04-08 19:04:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-10 12:13:48 +0200 |
| commit | 7d614710615f15035ae6750babbf37b0ce7206d7 (patch) | |
| tree | b2727612b23f7dd2283c3b2a5df84320c626b08d /doc/plugin_tutorial/tuto3 | |
| parent | e34cae33d494f4ad1a4a27c94a323a160dc67d9f (diff) | |
Coqide completion: Avoiding using an iterator in an apparently sensitive code.
Let's see if it fixes #11943. See there for explanations about the
related segfault.
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
0 files changed, 0 insertions, 0 deletions