author | wenzelm |
Tue, 11 Sep 2012 11:03:59 +0200 | |
changeset 49251 | cd28155bb7d5 |
parent 49250 | 332ab3748350 |
child 49252 | 9e10481dd3c4 |
--- 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() } }