proper etc/preferences;
authorwenzelm
Sun Apr 07 12:41:52 2019 +0200 (5 months ago)
changeset 70075ee0b8e06b01c
parent 70074 b718a64d0d09
child 70076 3b3089863eda
proper etc/preferences;
NEWS
     1.1 --- a/NEWS	Sat Apr 06 22:26:38 2019 +0200
     1.2 +++ b/NEWS	Sun Apr 07 12:41:52 2019 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4  * Isabelle DejaVu fonts are available with hinting by default, which is
     1.5  relevant for low-resolution displays. This may be disabled via system
     1.6  option "isabelle_fonts_hinted = false" in
     1.7 -$ISABELLE_HOME_USER/etc/settings -- it occasionally yields better
     1.8 +$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
     1.9  results.
    1.10  
    1.11  * OpenJDK 11 has quite different font rendering, with better glyph