| changeset 70075 | ee0b8e06b01c |
| parent 70072 | 54dc58086351 |
| child 70080 | 36821db2e356 |
--- a/NEWS Sat Apr 06 22:26:38 2019 +0200 +++ b/NEWS Sun Apr 07 12:41:52 2019 +0200 @@ -93,7 +93,7 @@ * Isabelle DejaVu fonts are available with hinting by default, which is relevant for low-resolution displays. This may be disabled via system option "isabelle_fonts_hinted = false" in -$ISABELLE_HOME_USER/etc/settings -- it occasionally yields better +$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better results. * OpenJDK 11 has quite different font rendering, with better glyph