src/Pure/Tools/build_process.scala
changeset 78633 37a0c953649d
parent 78632 e3d7793545df
child 78635 26a02b042fe0
--- a/src/Pure/Tools/build_process.scala	Sun Sep 03 12:30:44 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Sep 03 12:39:19 2023 +0200
@@ -25,6 +25,10 @@
     sessions: List[String]
   ) {
     def active: Boolean = stop.isEmpty
+
+    def print: String =
+      build_uuid + " (platform: " + ml_platform + ", start: " + Build_Log.print_date(start) +
+        if_proper(stop, ", stop: " + Build_Log.print_date(stop.get)) + ")"
   }
 
   sealed case class Worker(