src/Tools/jEdit/src/jEdit.props
changeset 72253 1b01c626a441
parent 72249 4bf8a8a2d2ad
child 72930 0cc298e29aff
equal deleted inserted replaced
72252:3b17e7688dc6 72253:1b01c626a441
   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.memory.background=#666699
   340 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
   341 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
   341 view.thickCaret=true
   342 view.thickCaret=true
   342 view.width=1200
   343 view.width=1200
   343 xml-insert-closing-tag.shortcut=
   344 xml-insert-closing-tag.shortcut=