src/Tools/jEdit/src/jEdit.props
changeset 72139 f5c085dfa02f
parent 71571 f36886cc32fa
child 72249 4bf8a8a2d2ad
equal deleted inserted replaced
72138:fa57d299b46b 72139:f5c085dfa02f
   335 view.gutter.lineNumbers=false
   335 view.gutter.lineNumbers=false
   336 view.gutter.selectionAreaWidth=18
   336 view.gutter.selectionAreaWidth=18
   337 view.height=850
   337 view.height=850
   338 view.middleMousePaste=true
   338 view.middleMousePaste=true
   339 view.showToolbar=true
   339 view.showToolbar=true
       
   340 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor memory-status ml-status errors clock
   340 view.thickCaret=true
   341 view.thickCaret=true
   341 view.width=1200
   342 view.width=1200
   342 xml-insert-closing-tag.shortcut=
   343 xml-insert-closing-tag.shortcut=