more portable alternative shortcuts on numeric keypad;
authorwenzelm
Mon, 28 Jan 2013 22:37:58 +0100
changeset 520372f50ddd3b586
parent 52036 48cecc50c221
child 52038 6ca703425c01
more portable alternative shortcuts on numeric keypad;
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Jan 28 17:37:09 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Jan 28 22:37:58 2013 +0100
     1.3 @@ -197,9 +197,10 @@
     1.4  isabelle.control-reset.label=Control reset
     1.5  isabelle.control-reset.shortcut=C+e LEFT
     1.6  isabelle.decrease-font-size.label=Decrease font size
     1.7 +isabelle.decrease-font-size.shortcut2=C+SUBTRACT
     1.8  isabelle.decrease-font-size.shortcut=C+MINUS
     1.9  isabelle.increase-font-size.label=Increase font size
    1.10 -isabelle.increase-font-size.shortcut2=C+EQUALS
    1.11 +isabelle.increase-font-size.shortcut2=C+ADD
    1.12  isabelle.increase-font-size.shortcut=C+PLUS
    1.13  lang.usedefaultlocale=false
    1.14  largefilemode=full