# HG changeset patch
# User wenzelm
# Date 1609712192 -3600
# Node ID 382309d4b4dcb3ad1692f2c185416be286477907
# Parent  4b1cfbf96e36de5413764af83764565980114f25
alternative shortcut, notably for macOS;

diff -r 4b1cfbf96e36 -r 382309d4b4dc src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sun Jan 03 23:06:37 2021 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Jan 03 23:16:32 2021 +0100
@@ -260,6 +260,7 @@
 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
 isabelle.toggle-full-screen.label=Toggle full-screen mode
 isabelle.toggle-full-screen.shortcut=F11
+isabelle.toggle-full-screen.shortcut2=S+F11
 isabelle.toggle-node-required.label=Toggle node required
 isabelle.toggle-node-required.shortcut=C+e SPACE
 isabelle.tooltip.label=Show tooltip