--- 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(", ", ", ")")
--- 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))
}