changeset 56662 | f373fb77e0a4 |
parent 56622 | 891d1b8b64fb |
child 56715 | 52125652e82a |
--- a/src/Tools/jEdit/src/find_dockable.scala Tue Apr 22 23:31:45 2014 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Tue Apr 22 23:49:15 2014 +0200 @@ -54,7 +54,7 @@ private def handle_resize() { - Swing_Thread.require() + Swing_Thread.require {} pretty_text_area.resize( Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))