--- 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