refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
authorwenzelm
Mon Apr 07 16:37:57 2014 +0200 (2014-04-07)
changeset 5645016d4213d4cbc
parent 56449 f0592485b7fb
child 56451 856492b0f755
child 56457 eea4bbe15745
refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
NEWS
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/NEWS	Mon Apr 07 13:55:12 2014 +0200
     1.2 +++ b/NEWS	Mon Apr 07 16:37:57 2014 +0200
     1.3 @@ -108,8 +108,7 @@
     1.4  simplification process, enabled by the newly-introduced
     1.5  "simplifier_trace" declaration.
     1.6  
     1.7 -* Support for Navigator plugin, with toolbar buttons and keyboard
     1.8 -shortcuts similar to major web browsers.
     1.9 +* Support for Navigator plugin (with toolbar buttons).
    1.10  
    1.11  
    1.12  *** Pure ***
     2.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Apr 07 13:55:12 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Apr 07 16:37:57 2014 +0200
     2.3 @@ -227,8 +227,6 @@
     2.4  logo.icon.medium=32x32/apps/isabelle.gif
     2.5  lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
     2.6  match-bracket.shortcut2=C+9
     2.7 -navigator.back.shortcut=A+LEFT
     2.8 -navigator.forward.shortcut=A+RIGHT
     2.9  navigator.showOnToolbar=true
    2.10  next-bracket.shortcut2=C+e C+9
    2.11  plugin-blacklist.MacOSX.jar=true