diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2019-09-23 09:46:15 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-23 09:46:15 +0200 |
| commit | 80a3a78ee93b574733d02d20521f5b640c7fa936 (patch) | |
| tree | 9447b913c230862eef19e5c2c8ba04d258fc51a4 /thirdparty | |
| parent | 16bedc7edec42bb48e88abdb5787c015ed5ad191 (diff) | |
| parent | 481dbceed0d0610a6c689e3be448b7953994763e (diff) | |
Merge pull request #32043 from guilhermefelipecgs/fuzzy_help_search
Adds fuzzy search for help search dialog
Diffstat (limited to 'thirdparty')
0 files changed, 0 insertions, 0 deletions