# HG changeset patch
# User wenzelm
# Date 1380905507 -7200
# Node ID 2828f17fa41afd9c8ff6aac38321a8eafbc63ad5
# Parent  d2def195bb6b94303ca474ccad5983b516a3df65
another shortcut alias;

diff -r d2def195bb6b -r 2828f17fa41a 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