odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
authorwenzelm
Thu, 13 Dec 2012 20:39:07 +0100
changeset 50506 7d8406ebe18f
parent 50505 33c92722cc3d
child 50509 4a389d115b4f
odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
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