cancel already running request;
authorwenzelm
Tue, 03 Nov 2015 11:24:42 +0100
changeset 61555 e27cfd2bf094
parent 61551 078c9fd2e052
child 61556 0d4ee4168e41
cancel already running request;
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))