another shortcut alias;
authorwenzelm
Fri, 04 Oct 2013 18:51:47 +0200
changeset 54306 2828f17fa41a
parent 54305 d2def195bb6b
child 54307 903ab115e9fd
another shortcut alias;
src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Fri Oct 04 13:17:49 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Oct 04 18:51:47 2013 +0200
@@ -211,6 +211,7 @@
 isabelle.increase-font-size2.shortcut=C+EQUALS
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size
+isabelle.reset-font-size.shortcut2=C+NUMPAD0
 isabelle.reset-font-size.shortcut=C+0
 isabelle.reset-node-required.label=Reset node required
 isabelle.set-continuous-checking.label=Set continuous checking