--- 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
}
}
--- 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(