changeset 56667 | 65e84b0ef974 |
parent 56387 | d92eb5c3960d |
child 56730 | e723f041b6d0 |
--- a/src/Pure/System/invoke_scala.scala Wed Apr 23 11:40:42 2014 +0200 +++ b/src/Pure/System/invoke_scala.scala Wed Apr 23 12:39:23 2014 +0200 @@ -58,7 +58,7 @@ Exn.capture { f(arg) } match { case Exn.Res(null) => (Tag.NULL, "") case Exn.Res(res) => (Tag.OK, res) - case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "") + case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "") case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) } case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))