--- a/src/Pure/Tools/build_cluster.scala Thu Aug 10 16:57:01 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Thu Aug 10 19:42:21 2023 +0200
@@ -226,7 +226,10 @@
def capture[A](host: Build_Cluster.Host, op: String)(
e: => A,
msg: String = host.message(op + " ..."),
- err: Throwable => String = { exn => return_code(exn); host.message("failed to " + op) }
+ err: Throwable => String = { exn =>
+ return_code(exn)
+ host.message("failed to " + op + "\n" + Exn.print(exn))
+ }
): Exn.Result[A] = {
progress.capture(e, msg = msg, err = err)
}