more informative error;
authorwenzelm
Thu, 10 Aug 2023 19:42:21 +0200
changeset 78506 14da1177d1c3
parent 78505 8cd399b25dac
child 78507 91817b2f3f55
more informative error;
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)
   }