tuned GUI: attempt to improve divider mobility;
authorwenzelm
Wed, 29 Jan 2025 21:25:44 +0100
changeset 82017 9a8d408492a7
parent 82016 6a241e374a67
child 82018 d104c6ad04ee
child 82026 57b4e44f5bc4
tuned GUI: attempt to improve divider mobility;
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