# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717779046 -7200
# Node ID 7a5bbc2e4bad9b14b528b5c5329d59026f71c852
# Parent  c19f44f6525a7f1b30775a3131d689bf66b19a54
build manager: echo error messages to server output;

diff -r c19f44f6525a -r 7a5bbc2e4bad src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 07 18:16:50 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 07 18:50:46 2024 +0200
@@ -612,7 +612,7 @@
           Future.fork(
             process_future.join_result match {
               case Exn.Res(process) => process.run()
-              case Exn.Exn(_) => Process_Result(Process_Result.RC.interrupt)
+              case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
             })
         new State(
           process_futures + (context.name -> process_future),
@@ -627,7 +627,7 @@
           yield name ->
             (future.join_result match {
               case Exn.Res(result) => result
-              case Exn.Exn(_) => Process_Result(Process_Result.RC.interrupt)
+              case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
             })
 
         val process_futures1 = process_futures.filterNot((name, _) => finished.contains(name))
@@ -734,7 +734,9 @@
         val job = _state.running(name)
         val result = Result(job.kind, job.number, Status.from_result(process_result), Some(job.id))
 
-        echo("Finished job " + job.id + " with status code " + process_result.rc)
+        val interrupted_error = process_result.interrupted && process_result.err.nonEmpty
+        val err_msg = if_proper(interrupted_error, ": " + process_result.err)
+        echo("Finished job " + job.id + " with status code " + process_result.rc + err_msg)
 
         _state = _state
           .remove_running(job.name)