src/Pure/Tools/build.scala

--- a/src/Pure/Tools/build.scala	Tue May 14 16:45:09 2013 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 14 16:54:47 2013 +0200
@@ -721,6 +721,7 @@
       }
       catch {
         case ERROR(msg) => ignore_error(msg)
+        case exn: java.lang.Error => ignore_error(Exn.message(exn))
         case _: XML.XML_Atom | _: XML.XML_Body => ignore_error("")
       }
     }