alternative shortcut, notably for macOS;
authorwenzelm
Sun, 03 Jan 2021 23:16:32 +0100
changeset 73281 382309d4b4dc
parent 73280 4b1cfbf96e36
child 73282 bf994dbe4941
child 73283 66b45c3389d3
alternative shortcut, notably for macOS;
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