diff -r 3d1746a716fa -r d70dc78c0d4e src/Pure/Tools/build_cluster.scala --- a/src/Pure/Tools/build_cluster.scala Sun Jul 23 20:45:00 2023 +0200 +++ b/src/Pure/Tools/build_cluster.scala Sun Jul 23 21:04:33 2023 +0200 @@ -115,7 +115,6 @@ } def message(msg: String): String = "Host " + quote(host.name) + if_proper(msg, ": " + msg) - def err_message(msg: String)(exn: Throwable): String = message(msg + "\n" + Exn.message(exn)) def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = { val session_options = build_context.build_options ++ host.options