proper default;
authorwenzelm
Fri, 05 Apr 2019 22:58:29 +0200
changeset 70069 381035c03220
parent 70068 1eed61c3a5e5
child 70070 673a9d008123
proper default;
NEWS
--- a/NEWS	Fri Apr 05 21:54:08 2019 +0200
+++ b/NEWS	Fri Apr 05 22:58:29 2019 +0200
@@ -55,8 +55,8 @@
 DejaVu" collection by default, which provides uniform rendering quality
 with the usual Isabelle symbols. Line spacing no longer needs to be
 adjusted: properties for the old IsabelleText font had "Global Options /
-Text Area / Extra vertical line spacing (in pixels): -2", now it
-defaults to 0.
+Text Area / Extra vertical line spacing (in pixels): -2", it now
+defaults to 1, but 0 works as well.
 
 * The jEdit File Browser is more prominent in the default GUI layout of
 Isabelle/jEdit: various virtual file-systems provide access to Isabelle