src/Pure/GUI/gui_thread.scala
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)