# HG changeset patch
# User wenzelm
# Date 1706648073 -3600
# Node ID 2ff1c4b92e2423bce1a58d30771c01ab3ed64ed3
# Parent  f1c754e60ea08310bee74d73be4dcacf7c34cd90
more informative message (amending b8a6b2ec85a2);

diff -r f1c754e60ea0 -r 2ff1c4b92e24 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Jan 30 21:47:37 2024 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Jan 30 21:54:33 2024 +0100
@@ -480,7 +480,8 @@
         res match {
           case Exn.Res(_) => None
           case Exn.Exn(exn) =>
-            Output.writeln("Exception trace for " + quote(task.name) + ":\n" + Exn.trace(exn))
+            Output.writeln("Exception trace for " + quote(task.name) + ":\n" +
+              Exn.message(exn) + "\n" + Exn.trace(exn))
             val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
             Some(first_line)
         }