diff options
author | RĂ©mi Verschelde <rverschelde@gmail.com> | 2017-11-29 08:58:56 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-29 08:58:56 +0100 |
commit | 6110235bd4fd95bc35b0beaa6023e5787d786242 (patch) | |
tree | da71c329cb32471c6c54735a99d854dbb90fe99b /doc/tools | |
parent | 76725b6c1f73c8d160ad91b42c803a54c78298d4 (diff) | |
parent | d6a95e154a507494efc51767d4535d8c36792d33 (diff) |
Merge pull request #13390 from poke1024/opteditorhelp
Make editor help select shortest (best) instead of first match
Diffstat (limited to 'doc/tools')
0 files changed, 0 insertions, 0 deletions