changeset 81493 | 07e79b80e96d |
parent 81486 | ed5e75468db3 |
child 81657 | 4210fd10e776 |
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Nov 19 15:35:03 2024 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Nov 19 15:46:22 2024 +0100 @@ -96,7 +96,8 @@ override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation - output.init_gui(dockable, split = true) + output.setup(dockable) + set_content(output.split_pane) /* tree view */