# HG changeset patch
# User wenzelm
# Date 1551301687 -3600
# Node ID a12d2eb58aca330711b9f37208c56ccefaeb6d75
# Parent  e02e3763e7a445c2e578bcde67a57d772f88c9a8
more line spacing, notably for ttfautohint (see 4791988fcbc4);

diff -r e02e3763e7a4 -r a12d2eb58aca src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed Feb 27 21:30:16 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Feb 27 22:08:07 2019 +0100
@@ -263,7 +263,7 @@
 options.shortcuts.duplicatekeymap.label=Duplicate
 options.shortcuts.resetkeymap.dialog.title=Reset keymap
 options.shortcuts.resetkeymap.label=Reset
-options.textarea.lineSpacing=0
+options.textarea.lineSpacing=1
 plugin-blacklist.MacOSX.jar=true
 plugin.MacOSXPlugin.altDispatcher=false
 plugin.MacOSXPlugin.disableOption=true