src/Tools/jEdit/src/jEdit.props
changeset 61529 82fc5a6231a2
parent 61526 c04295685936
child 62675 2f816b80e3f4
equal deleted inserted replaced
61528:053f7083b3eb 61529:82fc5a6231a2
   238 lang.usedefaultlocale=false
   238 lang.usedefaultlocale=false
   239 largefilemode=full
   239 largefilemode=full
   240 line-end.shortcut=END
   240 line-end.shortcut=END
   241 line-home.shortcut=HOME
   241 line-home.shortcut=HOME
   242 logo.icon.medium=32x32/apps/isabelle.gif
   242 logo.icon.medium=32x32/apps/isabelle.gif
   243 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
   243 lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
   244 match-bracket.shortcut2=C+9
   244 match-bracket.shortcut2=C+9
   245 navigator.showOnToolbar=true
   245 navigator.showOnToolbar=true
   246 next-bracket.shortcut2=C+e C+9
   246 next-bracket.shortcut2=C+e C+9
   247 options.textarea.lineSpacing=-2
   247 options.textarea.lineSpacing=-2
   248 plugin-blacklist.MacOSX.jar=true
   248 plugin-blacklist.MacOSX.jar=true