adapted to a8ee66876a1a;

--- 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=