more portable alternative shortcuts on numeric keypad;
authorwenzelm
Mon Jan 28 22:37:58 2013 +0100 (2013-01-28)
changeset 510692f50ddd3b586
parent 51068 48cecc50c221
child 51070 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