changeset 75809 | 1dd5d4f4b69e |
parent 75393 | 87ebf5a50283 |
child 75810 | 51867c8ad109 |
--- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Aug 12 11:26:09 2022 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Aug 12 11:35:44 2022 +0200 @@ -268,7 +268,7 @@ selected = false } - private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } + private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() } private val controls = Wrap_Panel(