# HG changeset patch
# User wenzelm
# Date 1368543287 -7200
# Node ID 5fdca5bfc0b4644fb2a96aced644fc52d7e485ea
# Parent  f6c04bf0123d213fa634f7aace7c5c8135f65d28
more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError;

diff -r f6c04bf0123d -r 5fdca5bfc0b4 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("")
       }
     }