changeset 56860 | dc71c3d0e909 |
parent 56782 | 433cf57550fa |
child 56861 | 5f827142d89a |
--- a/src/Pure/General/exn.scala Sun May 04 21:35:04 2014 +0200 +++ b/src/Pure/General/exn.scala Mon May 05 09:24:34 2014 +0200 @@ -45,6 +45,8 @@ def apply(): Throwable = new InterruptedException def unapply(exn: Throwable): Boolean = is_interrupt(exn) + def expose(): Unit = if (Thread.interrupted()) throw apply() + val return_code = 130 }