src/Pure/Tools/build_cluster.scala

--- a/src/Pure/Tools/build_cluster.scala	Tue Jul 18 23:03:39 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Wed Jul 19 10:42:40 2023 +0200
@@ -22,6 +22,8 @@
       numa: Boolean = false,
       options: List[Options.Spec] = Nil
     ): Host = new Host(host, user, port, jobs, numa, options)
+
+    def parse(str: String): Host = Host(host = str)  // FIXME proper parse
   }
 
   final class Host private(