# HG changeset patch
# User wenzelm
# Date 1446546282 -3600
# Node ID e27cfd2bf094019f82911b6f4fbd2f00af2c159d
# Parent  078c9fd2e052d820425a72942771b804474996ac
cancel already running request;

diff -r 078c9fd2e052 -r e27cfd2bf094 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Mon Nov 02 21:58:38 2015 +0100
+++ b/src/Pure/Concurrent/simple_thread.scala	Tue Nov 03 11:24:42 2015 +0100
@@ -71,7 +71,7 @@
       val new_run =
         running match {
           case Some(request) => if (first) false else { request.cancel; cancel(); true }
-          case None => true
+          case None => cancel(); true
         }
       if (new_run)
         running = Some(Event_Timer.request(Time.now() + delay)(run))