changeset 56662 | f373fb77e0a4 |
parent 55827 | 8a881f83e206 |
child 57044 | 042d6e58cb40 |
--- a/src/Tools/jEdit/src/font_info.scala Tue Apr 22 23:31:45 2014 +0200 +++ b/src/Tools/jEdit/src/font_info.scala Tue Apr 22 23:49:15 2014 +0200 @@ -42,7 +42,7 @@ { private def change_size(change: Float => Float) { - Swing_Thread.require() + Swing_Thread.require {} val size0 = main_size() val size = restrict_size(change(size0)).round