proper etc/preferences;
authorwenzelm
Sun, 07 Apr 2019 12:41:52 +0200
changeset 70258 ee0b8e06b01c
parent 70256 b718a64d0d09
child 70259 3b3089863eda
proper etc/preferences;
NEWS
--- 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