src/Pure/System/swing_thread.scala
changeset 49251 cd28155bb7d5
parent 49249 c763444b34ad
child 52477 025b3777e592
--- a/src/Pure/System/swing_thread.scala	Mon Sep 10 21:17:32 2012 +0200
+++ b/src/Pure/System/swing_thread.scala	Tue Sep 11 11:03:59 2012 +0200
@@ -83,7 +83,7 @@
       {
         require()
         if (timer.isRunning) {
-          timer.setInitialDelay(timer.getDelay max alt_time.ms.toInt)
+          timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
           timer.restart()
         }
       }