src/Pure/Tools/build.scala
changeset 56861 5f827142d89a
parent 56860 dc71c3d0e909
child 56871 d06ff36b4fa7
     1.1 --- a/src/Pure/Tools/build.scala	Mon May 05 09:24:34 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon May 05 09:41:23 2014 +0200
     1.3 @@ -814,7 +814,7 @@
     1.4      def sleep()
     1.5      {
     1.6        try { Thread.sleep(500) }
     1.7 -      catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
     1.8 +      catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
     1.9      }
    1.10  
    1.11      @tailrec def loop(