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(