# HG changeset patch
# User wenzelm
# Date 1680118128 -7200
# Node ID 1208ece65cca923d4fcfdb2b8f8c5001465374b0
# Parent  7ac59361791e5a5eb0647966647f332a7c663079
more informative errors;

diff -r 7ac59361791e -r 1208ece65cca src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed Mar 29 21:23:56 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Mar 29 21:28:48 2023 +0200
@@ -992,7 +992,7 @@
     ): Multi_Map[String, String] = {
       var errors1 = errors
       def add_error(name: String, exn: Throwable): Unit = {
-        errors1 = errors1.insert(name, Exn.message(exn))
+        errors1 = errors1.insert(name, Exn.print(exn))
       }
 
       abstract class Table_Status(table: SQL.Table) {