src/Tools/jEdit/src/debugger_dockable.scala
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 */