author | wenzelm |
Wed, 29 Jan 2025 21:25:44 +0100 | |
changeset 82017 | 9a8d408492a7 |
parent 82016 | 6a241e374a67 |
child 82018 | d104c6ad04ee |
child 82026 | 57b4e44f5bc4 |
--- 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