clarified signature;
authorwenzelm
Wed, 14 Feb 2024 11:08:05 +0100
changeset 79602 9ba800f12785
parent 79601 3430787e0620
child 79603 9f002cdb6b8d
clarified signature;
src/Pure/System/benchmark.scala
src/Pure/System/host.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)))
       }
     }
   }
--- 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 */