# HG changeset patch
# User wenzelm
# Date 1396881477 -7200
# Node ID 16d4213d4cbc9db20ab4187ddc10cb00647fe702
# Parent  f0592485b7fbb60d5042097151b7133cbeb5b618
refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;

diff -r f0592485b7fb -r 16d4213d4cbc NEWS
--- 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 ***
diff -r f0592485b7fb -r 16d4213d4cbc src/Tools/jEdit/src/jEdit.props
--- 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