author | wenzelm |
Sat, 23 Feb 2013 17:12:48 +0100 | |
changeset 51255 | 9db9e8c608ea |
parent 51254 | 5bae6fc0e125 |
child 51256 | ee836df361ed |
--- a/src/Pure/General/exn.scala Sat Feb 23 15:08:53 2013 +0100 +++ b/src/Pure/General/exn.scala Sat Feb 23 17:12:48 2013 +0100 @@ -44,7 +44,9 @@ else None def message(exn: Throwable): String = - user_message(exn) getOrElse exn.toString + user_message(exn) getOrElse + (if (exn.isInstanceOf[InterruptedException]) "Interrupt" + else exn.toString) /* recover from spurious crash */