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)) }