diff options
| author |  Dirk Hohndel <dirk@hohndel.org> | 2021-01-15 06:02:18 -0800 |
|---|---|---|
| committer | Dirk Hohndel <dirk@hohndel.org> | 2021-01-19 12:35:29 -0800 |
| commit | f26f71a80b13a9ddf9428e520d74043747432e10 (patch) | |
| tree | 7d2de9290bf5506e24b0a60a26ee854af2dd157e /icons/pref_equipment.png | |
| parent | 323e97c60370f06bb30e57580c8c4fce39df95f7 (diff) | |
| download | subsurface-f26f71a80b13a9ddf9428e520d74043747432e10.tar.gz | |
mobile/UI: fix font size when OS font is given in px
Android appears to set its default font in pixels, not points. So guess
the point size based on the font metric information. This is not
perfect, but creates results that are good enough.
Signed-off-by: Dirk Hohndel <dirk@hohndel.org>
Diffstat (limited to 'icons/pref_equipment.png')
0 files changed, 0 insertions, 0 deletions