tuned output;
authorwenzelm
Sun, 05 Mar 2023 19:33:01 +0100
changeset 77526 e3ed231fa214
parent 77525 de6fb423fd4b
child 77527 790085b1002f
tuned output;
src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Sun Mar 05 19:21:07 2023 +0100
+++ b/src/Pure/System/host.scala	Sun Mar 05 19:33:01 2023 +0100
@@ -16,7 +16,10 @@
 
   object Node_Info { def none: Node_Info = Node_Info("", None) }
 
-  sealed case class Node_Info(hostname: String, numa_node: Option[Int])
+  sealed case class Node_Info(hostname: String, numa_node: Option[Int]) {
+    override def toString: String =
+      hostname + if_proper(numa_node, "/" + numa_node.get.toString)
+  }
 
 
   /* available NUMA nodes */