# HG changeset patch
# User wenzelm
# Date 1678041181 -3600
# Node ID e3ed231fa2140393ff5348831fd8405899f01bf4
# Parent  de6fb423fd4bfa9bf9ae208daf8c5ac04fa84d82
tuned output;

diff -r de6fb423fd4b -r e3ed231fa214 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 */