uniform operation on initial delay;
authorwenzelm
Tue, 11 Sep 2012 11:03:59 +0200
changeset 49251 cd28155bb7d5
parent 49250 332ab3748350
child 49252 9e10481dd3c4
uniform operation on initial delay;
src/Pure/System/swing_thread.scala
--- 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()
         }
       }