another shortcut alias;
authorwenzelm
Fri, 04 Oct 2013 18:51:47 +0200
changeset 551942828f17fa41a
parent 55193 d2def195bb6b
child 55195 903ab115e9fd
another shortcut alias;
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Oct 04 13:17:49 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Oct 04 18:51:47 2013 +0200
     1.3 @@ -211,6 +211,7 @@
     1.4  isabelle.increase-font-size2.shortcut=C+EQUALS
     1.5  isabelle.reset-continuous-checking.label=Reset continuous checking
     1.6  isabelle.reset-font-size.label=Reset font size
     1.7 +isabelle.reset-font-size.shortcut2=C+NUMPAD0
     1.8  isabelle.reset-font-size.shortcut=C+0
     1.9  isabelle.reset-node-required.label=Reset node required
    1.10  isabelle.set-continuous-checking.label=Set continuous checking