# HG changeset patch
# User wenzelm
# Date 1359409078 -3600
# Node ID 2f50ddd3b5860b830d65cb6e81c83d79c8204c98
# Parent  48cecc50c221da9b2798e6b702c0ed9688ac274b
more portable alternative shortcuts on numeric keypad;

diff -r 48cecc50c221 -r 2f50ddd3b586 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Jan 28 17:37:09 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Jan 28 22:37:58 2013 +0100
@@ -197,9 +197,10 @@
 isabelle.control-reset.label=Control reset
 isabelle.control-reset.shortcut=C+e LEFT
 isabelle.decrease-font-size.label=Decrease font size
+isabelle.decrease-font-size.shortcut2=C+SUBTRACT
 isabelle.decrease-font-size.shortcut=C+MINUS
 isabelle.increase-font-size.label=Increase font size
-isabelle.increase-font-size.shortcut2=C+EQUALS
+isabelle.increase-font-size.shortcut2=C+ADD
 isabelle.increase-font-size.shortcut=C+PLUS
 lang.usedefaultlocale=false
 largefilemode=full