# HG changeset patch
# User wenzelm
# Date 1738182344 -3600
# Node ID 9a8d408492a78743d6157fdeaa369488d9b3f227
# Parent  6a241e374a67fdd238809df74d5743e029da399b
tuned GUI: attempt to improve divider mobility;

diff -r 6a241e374a67 -r 9a8d408492a7 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Wed Jan 29 20:52:27 2025 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Wed Jan 29 21:25:44 2025 +0100
@@ -137,6 +137,7 @@
 
   lazy val split_pane: SplitPane =
     new SplitPane(Orientation.Vertical) {
+      resizeWeight = 0.5
       oneTouchExpandable = true
       leftComponent = tree_pane
       rightComponent = text_pane