adapted to a8ee66876a1a;
authorwenzelm
Thu, 31 Jan 2019 16:56:31 +0100
changeset 69790 8608928e54ab
parent 69789 ca9780325a21
child 69791 5a8ae7a4b7d0
adapted to a8ee66876a1a;
src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Jan 31 16:53:15 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Thu Jan 31 16:56:31 2019 +0100
@@ -317,9 +317,9 @@
 view.gutter.fontsize=12
 view.gutter.lineNumbers=false
 view.gutter.selectionAreaWidth=18
-view.height=787
+view.height=850
 view.middleMousePaste=true
 view.showToolbar=true
 view.thickCaret=true
-view.width=1072
+view.width=1200
 xml-insert-closing-tag.shortcut=