changeset 56860 | dc71c3d0e909 |
parent 56770 | e160ae47db94 |
child 59136 | c2b23cb8a677 |
--- a/src/Pure/Concurrent/simple_thread.scala Sun May 04 21:35:04 2014 +0200 +++ b/src/Pure/Concurrent/simple_thread.scala Mon May 05 09:24:34 2014 +0200 @@ -16,12 +16,6 @@ object Simple_Thread { - /* pending interrupts */ - - def interrupted_exception(): Unit = - if (Thread.interrupted()) throw Exn.Interrupt() - - /* plain thread */ def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =