tuned signature;

--- a/src/Pure/Tools/build_cluster.scala	Fri Jul 21 13:02:07 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Fri Jul 21 14:14:48 2023 +0200
@@ -84,12 +84,12 @@
   }
 
   final class Host private(
-    name: String,
-    user: String,
-    port: Int,
-    jobs: Int,
-    numa: Boolean,
-    options: List[Options.Spec]
+    val name: String,
+    val user: String,
+    val port: Int,
+    val jobs: Int,
+    val numa: Boolean,
+    val options: List[Options.Spec]
   ) {
     def is_local: Boolean = SSH.is_local(name)