changeset 75809 | 1dd5d4f4b69e |
parent 75393 | 87ebf5a50283 |
child 75810 | 51867c8ad109 |
--- a/src/Tools/jEdit/src/state_dockable.scala Fri Aug 12 11:26:09 2022 +0200 +++ b/src/Tools/jEdit/src/state_dockable.scala Fri Aug 12 11:35:44 2022 +0200 @@ -98,7 +98,7 @@ reactions += { case ButtonClicked(_) => print_state.locate_query() } } - 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(