# HG changeset patch
# User wenzelm
# Date 1707997320 -3600
# Node ID 50ec6a68d36fdb8ea31d50c1b4d8710d680022e3
# Parent  50376abd132dbebd74c7881f30dd8d4be85858a4
tuned signature;

diff -r 50376abd132d -r 50ec6a68d36f src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Thu Feb 15 12:37:52 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Thu Feb 15 12:42:00 2024 +0100
@@ -119,6 +119,7 @@
 
     def ssh_host: String = proper_string(hostname) getOrElse name
     def is_local: Boolean = SSH.is_local(ssh_host)
+    def is_remote: Boolean = !is_local
 
     override def toString: String = print
 
@@ -224,7 +225,7 @@
   }
 
   def make(build_context: Build.Context, progress: Progress = new Progress): Build_Cluster = {
-    val remote_hosts = build_context.build_hosts.filterNot(_.is_local)
+    val remote_hosts = build_context.build_hosts.filter(_.is_remote)
     if (remote_hosts.isEmpty) none
     else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress)
   }
@@ -252,7 +253,7 @@
   val remote_hosts: List[Build_Cluster.Host],
   val progress: Progress = new Progress
 ) extends Build_Cluster {
-  require(remote_hosts.nonEmpty && !remote_hosts.exists(_.is_local), "remote hosts required")
+  require(remote_hosts.nonEmpty && remote_hosts.forall(_.is_remote), "remote hosts required")
 
   override def toString: String =
     remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")")