author | wenzelm |
Tue, 03 Nov 2015 11:24:42 +0100 | |
changeset 61555 | e27cfd2bf094 |
parent 61552 | 078c9fd2e052 |
child 61556 | 0d4ee4168e41 |
--- 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))