--- 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 */