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() } }