# HG changeset patch
# User wenzelm
# Date 1355427547 -3600
# Node ID 7d8406ebe18f22364800db3513e69d424e66878a
# Parent  33c92722cc3d9ef83a81fbd3c1c120e308c39acf
odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;

diff -r 33c92722cc3d -r 7d8406ebe18f src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Thu Dec 13 20:39:07 2012 +0100
@@ -191,8 +191,8 @@
 isabelle.control-bold.shortcut=C+e RIGHT
 isabelle.control-isub.label=Control subscript
 isabelle.control-isub.shortcut=C+e DOWN
-isabelle.control-isup.label=Control superscript
-isabelle.control-isup.shortcut=C+e UP
+isabelle.control-sup.label=Control superscript
+isabelle.control-sup.shortcut=C+e UP
 isabelle.control-reset.label=Control reset
 isabelle.control-reset.shortcut=C+e LEFT
 isabelle.decrease-font-size.label=Decrease font size