| changeset 69774 | 8608928e54ab |
| parent 69773 | ca9780325a21 |
| child 69781 | a7529ac9c1c5 |
--- 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=