diff -r 8cd399b25dac -r 14da1177d1c3 src/Pure/Tools/build_cluster.scala --- 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) }