unused;
authorwenzelm
Sun, 23 Jul 2023 21:04:33 +0200
changeset 78445 d70dc78c0d4e
parent 78444 3d1746a716fa
child 78446 9067d8ac9c47
unused;
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