author | wenzelm |
Wed, 27 Feb 2019 22:08:07 +0100 | |
changeset 69847 | a12d2eb58aca |
parent 69846 | e02e3763e7a4 |
child 69848 | bf2cd27714fb |
--- 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