diff -r e3bad2e60f65 -r 01b548a504dc src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Fri Nov 07 16:43:04 2025 +0100 +++ b/src/Pure/System/bash.scala Fri Nov 07 16:55:23 2025 +0100 @@ -321,6 +321,14 @@ server.start() server } + + def result(result: Process_Result): List[String] = + result.rc.toString :: + result.timing.elapsed.ms.toString :: + result.timing.cpu.ms.toString :: + result.out_lines.length.toString :: + result.out_lines ::: + result.err_lines } class Server private(port: Int, debugging: => Boolean) @@ -345,14 +353,7 @@ else List(Server.FAILURE, Exn.message(exn))) def reply_result(result: Process_Result): Unit = - reply( - Server.RESULT :: - result.rc.toString :: - result.timing.elapsed.ms.toString :: - result.timing.cpu.ms.toString :: - result.out_lines.length.toString :: - result.out_lines ::: - result.err_lines) + reply(Server.RESULT :: Server.result(result)) connection.read_byte_message().map(_.map(_.text)) match { case None =>