# HG changeset patch
# User wenzelm
# Date 1347354239 -7200
# Node ID cd28155bb7d5bd0e683b977f854f8355f44410ab
# Parent  332ab3748350fa836a78aff3ed89dbc01316189a
uniform operation on initial delay;

diff -r 332ab3748350 -r cd28155bb7d5 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()
         }
       }