# HG changeset patch
# User wenzelm
# Date 1610888423 -3600
# Node ID c98a2f82b95032ea2a7215234edcf264e725b790
# Parent  d0c8e8ca3505a71c662fe86e243269a3e441f173
more robust GUI, notably for Big Sur full-screen where the hypersearch panel becomes a separate maximized window;

diff -r d0c8e8ca3505 -r c98a2f82b950 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sun Jan 17 11:19:15 2021 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Jan 17 14:00:23 2021 +0100
@@ -187,6 +187,7 @@
 helpviewer.font=Isabelle DejaVu Serif
 helpviewer.fontsize=12
 home.shortcut=
+hypersearch-results.dock-position=right
 insert-newline-indent.shortcut=
 insert-newline.shortcut=
 isabelle-debugger.dock-position=floating