refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
authorwenzelm
Mon, 07 Apr 2014 16:37:57 +0200
changeset 56450 16d4213d4cbc
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
--- a/NEWS	Mon Apr 07 13:55:12 2014 +0200
+++ b/NEWS	Mon Apr 07 16:37:57 2014 +0200
@@ -108,8 +108,7 @@
 simplification process, enabled by the newly-introduced
 "simplifier_trace" declaration.
 
-* Support for Navigator plugin, with toolbar buttons and keyboard
-shortcuts similar to major web browsers.
+* Support for Navigator plugin (with toolbar buttons).
 
 
 *** Pure ***
--- a/src/Tools/jEdit/src/jEdit.props	Mon Apr 07 13:55:12 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Apr 07 16:37:57 2014 +0200
@@ -227,8 +227,6 @@
 logo.icon.medium=32x32/apps/isabelle.gif
 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
 match-bracket.shortcut2=C+9
-navigator.back.shortcut=A+LEFT
-navigator.forward.shortcut=A+RIGHT
 navigator.showOnToolbar=true
 next-bracket.shortcut2=C+e C+9
 plugin-blacklist.MacOSX.jar=true