# HG changeset patch
# User wenzelm
# Date 1689931303 -7200
# Node ID e5908be41a36931fab676a01ca63dff6e339340f
# Parent  645b54f3244a5738843dd41aacf9a76453bf5024
clarified signature (again);
more explicit "local" name;

diff -r 645b54f3244a -r e5908be41a36 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Fri Jul 21 11:11:50 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Fri Jul 21 11:21:43 2023 +0200
@@ -12,6 +12,8 @@
   /* host specifications */
 
   object Host {
+    val LOCAL = "local"
+
     private val rfc822_specials = """()<>@,;:\"[]"""
 
     private val USER = "user"
@@ -77,7 +79,7 @@
     numa: Boolean,
     options: List[Options.Spec]
   ) {
-    def is_remote: Boolean = name.nonEmpty
+    def is_local: Boolean = name.isEmpty || name == Host.LOCAL
 
     override def toString: String = print
 
@@ -91,9 +93,7 @@
         ).filter(_.nonEmpty)
       val rest = (params ::: options).mkString(",")
 
-      if (name.isEmpty) ":" + rest
-      else if (rest.isEmpty) name
-      else name + ":" + rest
+      (if (is_local) Host.LOCAL else name) + if_proper(rest, ":" + rest)
     }
 
     def open_ssh_session(options: Options): SSH.Session =
@@ -114,7 +114,7 @@
   remote_hosts: List[Build_Cluster.Host],
   progress: Progress = new Progress
 ) extends AutoCloseable {
-  require(remote_hosts.nonEmpty && remote_hosts.forall(_.is_remote), "remote hosts required")
+  require(remote_hosts.nonEmpty && !remote_hosts.exists(_.is_local), "remote hosts required")
 
   override def toString: String = remote_hosts.mkString("Build_Cluster(", ", ", ")")
 
diff -r 645b54f3244a -r e5908be41a36 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jul 21 11:11:50 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jul 21 11:21:43 2023 +0200
@@ -886,7 +886,7 @@
 
   private val _build_cluster =
     try {
-      val remote_hosts = build_context.build_hosts.filter(_.is_remote)
+      val remote_hosts = build_context.build_hosts.filterNot(_.is_local)
       if (build_context.master && _build_database.isDefined && remote_hosts.nonEmpty) {
         Some(init_cluster(remote_hosts))
       }