src/Pure/General/exn.scala
changeset 63782 aced4f0d1ad4
parent 62508 d0b68218ea55
child 64370 865b39487b5d
--- 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