author | wenzelm |
Sun, 04 Sep 2016 21:41:08 +0200 | |
changeset 63782 | aced4f0d1ad4 |
parent 63781 | af9fe0b6b78e |
child 63783 | baa20f3b6cea |
--- a/src/Pure/General/exn.scala Sun Sep 04 21:09:18 2016 +0200 +++ b/src/Pure/General/exn.scala Sun Sep 04 21:41:08 2016 +0200 @@ -124,6 +124,11 @@ val msg = exn.getMessage Some(if (msg == null || msg == "") "Error" else msg) } + else if (exn.isInstanceOf[java.sql.SQLException]) + { + val msg = exn.getMessage + Some(if (msg == null || msg == "") "SQL error" else msg) + } else if (exn.isInstanceOf[java.io.IOException]) { val msg = exn.getMessage