# HG changeset patch
# User wenzelm
# Date 1414335430 -3600
# Node ID e7d2b46520e057a56ff02fcbf06d3c71d5dda8df
# Parent  11d726ce599ea424c0d42740219039d648481d08
clarified default;

diff -r 11d726ce599e -r e7d2b46520e0 NEWS
--- a/NEWS	Sun Oct 26 15:46:02 2014 +0100
+++ b/NEWS	Sun Oct 26 15:57:10 2014 +0100
@@ -31,6 +31,9 @@
 interpreted semi-formally based on .bib files that happen to be opened
 in the editor (hyperlinks, completion etc.).
 
+* Less waste of vertical space via negative line spacing (see Global
+Options / Text Area).
+
 
 *** Pure ***
 
diff -r 11d726ce599e -r e7d2b46520e0 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sun Oct 26 15:46:02 2014 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Oct 26 15:57:10 2014 +0100
@@ -238,6 +238,7 @@
 match-bracket.shortcut2=C+9
 navigator.showOnToolbar=true
 next-bracket.shortcut2=C+e C+9
+options.textarea.lineSpacing=-2
 plugin-blacklist.MacOSX.jar=true
 plugin.MacOSXPlugin.altDispatcher=false
 plugin.MacOSXPlugin.disableOption=true