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() }
       }