src/Pure/System/host.scala
changeset 77526 e3ed231fa214
parent 77525 de6fb423fd4b
child 77541 9d9b30741fc4
--- 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 */