# HG changeset patch
# User wenzelm
# Date 1693737559 -7200
# Node ID 37a0c953649d1bc48515505fcd6c5228d30fef9b
# Parent  e3d7793545dfb7e0577f8b2618c6cc23172f721c
clarified signature;

diff -r e3d7793545df -r 37a0c953649d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Sep 03 12:30:44 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Sep 03 12:39:19 2023 +0200
@@ -477,12 +477,7 @@
     if (builds.isEmpty) "No build processes available" + print_database
     else {
       "Available build processes" + print_database +
-        (for ((build, i) <- builds.iterator.zipWithIndex)
-          yield {
-            "\n  " + build.build_uuid +
-              " (platform: " + build.ml_platform +
-              ", start: " + Build_Log.print_date(build.start) + ")"
-          }).mkString
+        (for (build <- builds.iterator) yield "\n  " + build.print).mkString
     }
   }
 
diff -r e3d7793545df -r 37a0c953649d src/Pure/Tools/build_process.scala
--- 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(