changeset 77752 | 1208ece65cca |
parent 77751 | 7ac59361791e |
child 77798 | 28c930aefb28 |
--- 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) {