src/Pure/Tools/build_process.scala
changeset 78424 e5908be41a36
parent 78421 fd24f380b588
child 78430 0461fc9d43e8
--- 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))
       }