--- a/src/Pure/General/exn.scala Mon May 05 09:24:34 2014 +0200
+++ b/src/Pure/General/exn.scala Mon May 05 09:41:23 2014 +0200
@@ -45,7 +45,8 @@
def apply(): Throwable = new InterruptedException
def unapply(exn: Throwable): Boolean = is_interrupt(exn)
- def expose(): Unit = if (Thread.interrupted()) throw apply()
+ def expose() { if (Thread.interrupted()) throw apply() }
+ def impose() { Thread.currentThread.interrupt }
val return_code = 130
}
--- a/src/Pure/Tools/build.scala Mon May 05 09:24:34 2014 +0200
+++ b/src/Pure/Tools/build.scala Mon May 05 09:41:23 2014 +0200
@@ -814,7 +814,7 @@
def sleep()
{
try { Thread.sleep(500) }
- catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
+ catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
}
@tailrec def loop(