diff options
| author | Hugo Herbelin | 2018-11-11 13:22:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-11 15:44:10 +0100 |
| commit | 3ccc9a89de9a2d5b81dae82c7815ba077f998135 (patch) | |
| tree | a4ee4a6809e04b368261564e3bcd4fa7872166a1 /dev/ci/ci-plugin-tutorial.sh | |
| parent | e17da6fc25eb7af0fbf59dfa6f1e3dd34c18edde (diff) | |
CoqIDE: remove obselete menu item "Complete word".
This was obsolete since new completion in 945d7db9 (then a07359f6).
Diffstat (limited to 'dev/ci/ci-plugin-tutorial.sh')
0 files changed, 0 insertions, 0 deletions