# HG changeset patch
# User wenzelm
# Date 1690139073 -7200
# Node ID d70dc78c0d4e43e1c09280044acbf027b95f20cf
# Parent  3d1746a716fab88398ea08f4ad15d0da7891f045
unused;

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