# HG changeset patch
# User wenzelm
# Date 1554633712 -7200
# Node ID ee0b8e06b01cf527118c82660e076892b37a21c1
# Parent  b718a64d0d09896b9258a14ea2ead0b0313e5929
proper etc/preferences;

diff -r b718a64d0d09 -r ee0b8e06b01c 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