# HG changeset patch
# User wenzelm
# Date 1678740235 -3600
# Node ID a4266d54ec35c930af01aa44a22387675c988e30
# Parent  afb1a19307c42d67f82a45b5eea2f02edd97b985
tuned output;

diff -r afb1a19307c4 -r a4266d54ec35 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 13 21:12:34 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 13 21:43:55 2023 +0100
@@ -820,6 +820,10 @@
   protected final val build_uuid: String = build_context.build_uuid
   protected final val worker_uuid: String = UUID.random().toString
 
+  override def toString: String =
+    "Build_Process(worker_uuid = " + quote(worker_uuid) + ", build_uuid = " + quote(build_uuid) +
+      if_proper(build_context.master, ", master = true") + ")"
+
 
   /* global state: internal var vs. external database */