diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2020-06-18 10:02:05 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-18 10:02:05 +0200 |
| commit | e54031cf1aa36022241fecca58258611f3319ef6 (patch) | |
| tree | e61a48a46f93daa447ac3605a97b5ded055c7a6c /editor/property_editor.h | |
| parent | a8fce16b2f675825b0f82889e2d5aca0c59b205c (diff) | |
| parent | a86521d0bdedc988d7c5a2892dc4d5cf7f01c793 (diff) | |
Merge pull request #39614 from hinlopen/fix-search-highlight
Search result highlights follow font size
Diffstat (limited to 'editor/property_editor.h')
0 files changed, 0 insertions, 0 deletions