# HG changeset patch
# User wenzelm
# Date 1399275683 -7200
# Node ID 5f827142d89a83e69b5a5e3c54c2c8ff265264f5
# Parent  dc71c3d0e90961720fc91d6c926b92b4ea6acc72
tuned signature;

diff -r dc71c3d0e909 -r 5f827142d89a src/Pure/General/exn.scala
--- 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
   }
diff -r dc71c3d0e909 -r 5f827142d89a src/Pure/Tools/build.scala
--- 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(