changeset 73340 | 0ffcad1f6130 |
parent 73120 | c3589f2dff31 |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/GUI/gui_thread.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/GUI/gui_thread.scala Mon Mar 01 22:22:12 2021 +0100 @@ -39,7 +39,7 @@ } } - def later(body: => Unit) + def later(body: => Unit): Unit = { if (SwingUtilities.isEventDispatchThread) body else SwingUtilities.invokeLater(() => body)