# HG changeset patch
# User wenzelm
# Date 1689941688 -7200
# Node ID 5b7d1cb073dbc2f3ff4589aec0b322b9c9c07057
# Parent  0be7e94fd24371fbc85e13ef2ccaf685fd35dcfa
tuned signature;

diff -r 0be7e94fd243 -r 5b7d1cb073db src/Pure/Tools/build_cluster.scala
--- 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)