# HG changeset patch
# User wenzelm
# Date 1707905285 -3600
# Node ID 9ba800f1278510049f809f8098cbada0f35f6268
# Parent  3430787e062076dfc57a8e1000268670475f3a37
clarified signature;

diff -r 3430787e0620 -r 9ba800f12785 src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Tue Feb 13 21:28:08 2024 +0100
+++ b/src/Pure/System/benchmark.scala	Wed Feb 14 11:08:05 2024 +0100
@@ -98,7 +98,7 @@
         progress.echo(
           "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
 
-        Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+        Host.write_info(db, Host.Info.init(hostname = hostname, score = Some(score)))
       }
     }
   }
diff -r 3430787e0620 -r 9ba800f12785 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Tue Feb 13 21:28:08 2024 +0100
+++ b/src/Pure/System/host.scala	Wed Feb 14 11:08:05 2024 +0100
@@ -135,15 +135,21 @@
     }
 
   object Info {
-    def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info =
-      Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
+    def init(
+      hostname: String = SSH.LOCAL,
+      ssh: SSH.System = SSH.Local,
+      score: Option[Double] = None
+    ): Info = Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
   }
 
   sealed case class Info(
     hostname: String,
     numa_nodes: List[Int],
     num_cpus: Int,
-    benchmark_score: Option[Double])
+    benchmark_score: Option[Double]
+  ) {
+    override def toString: String = hostname
+  }
 
 
   /* shuffling of NUMA nodes */