src/Tools/jEdit/src/jEdit.props
changeset 50492 8d8e882c7fbe
parent 50354 4a955d23c79b
child 50506 7d8406ebe18f
equal deleted inserted replaced
50491:0faaa279faee 50492:8d8e882c7fbe
   203 lang.usedefaultlocale=false
   203 lang.usedefaultlocale=false
   204 largefilemode=full
   204 largefilemode=full
   205 line-end.shortcut=END
   205 line-end.shortcut=END
   206 line-home.shortcut=HOME
   206 line-home.shortcut=HOME
   207 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
   207 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
       
   208 plugin.MacOSXPlugin.altDispatcher=true
       
   209 plugin.MacOSXPlugin.disableOption=true
   208 print.font=IsabelleText
   210 print.font=IsabelleText
   209 restore.remote=false
   211 restore.remote=false
   210 restore=false
   212 restore=false
   211 sidekick-tree.dock-position=right
   213 sidekick-tree.dock-position=right
   212 sidekick.auto-complete-popup-get-focus=true
   214 sidekick.auto-complete-popup-get-focus=true