# HG changeset patch
# User wenzelm
# Date 1659807451 -7200
# Node ID b33b19deca3a9a0930a9b54e7d5039aa57d425fa
# Parent  dba571dd0ba965d8a0992ac9d60d932279c6617b
clarified message;

diff -r dba571dd0ba9 -r b33b19deca3a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Aug 06 19:31:58 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sat Aug 06 19:37:31 2022 +0200
@@ -54,7 +54,7 @@
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
-            case _: XML.Error => ignore_error("")
+            case _: XML.Error => ignore_error("XML.Error")
           }
           finally { db.close() }
       }