diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-09-04 08:10:04 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-04 08:10:04 +0200 |
| commit | df11de72c9943955b874df89338fb7429a4e283c (patch) | |
| tree | 7b1cf9e6628ccb16b2ec31d9f070d24e1a5a592a /editor/editor_plugin.h | |
| parent | 8ebe6d83703858d2fa5f68555855ebc0b4730e17 (diff) | |
| parent | e298f931a614af94335069dc97878c09a986a478 (diff) | |
Merge pull request #10932 from djrm/pr_fix_metrics
Fixed some metrics (some issues caused by the new Noto Sans font).
Diffstat (limited to 'editor/editor_plugin.h')
0 files changed, 0 insertions, 0 deletions