# HG changeset patch
# User wenzelm
# Date 1708111224 -3600
# Node ID b3febd2a4c7312df60b428a4ac2431a50d681b6d
# Parent  8d2539a13502a552ed8ed821f90896a0f099f248
more robust: check subclasses as well;

diff -r 8d2539a13502 -r b3febd2a4c73 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 20:19:01 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 20:20:24 2024 +0100
@@ -55,7 +55,6 @@
       shared: Boolean = parameters.bool(SHARED),
       options: List[Options.Spec] = Nil
     ): Host = {
-      Path.split(dirs)  // check
       new Host(name, hostname, user, port, jobs, numa, dirs, home, shared, options)
     }
 
@@ -122,6 +121,8 @@
   ) {
     host =>
 
+    Path.split(host.dirs)  // check
+
     def ssh_host: String = proper_string(hostname) getOrElse name
     def is_local: Boolean = SSH.is_local(ssh_host)
     def is_remote: Boolean = !is_local