--- a/src/Pure/Build/build.scala Sun Mar 10 10:50:12 2024 +0100
+++ b/src/Pure/Build/build.scala Sun Mar 10 11:51:56 2024 +0100
@@ -523,7 +523,7 @@
val remove =
if (!remove_builds) Nil
else if (force) builds.map(_.build_uuid)
- else builds.flatMap(build => if (build.active) None else Some(build.build_uuid))
+ else builds.flatMap(_.active_build_uuid)
print(builds)
if (remove.nonEmpty) {
--- a/src/Pure/Build/build_process.scala Sun Mar 10 10:50:12 2024 +0100
+++ b/src/Pure/Build/build_process.scala Sun Mar 10 11:51:56 2024 +0100
@@ -25,6 +25,7 @@
sessions: List[String]
) {
def active: Boolean = stop.isEmpty
+ def active_build_uuid: Option[String] = if (active) Some(build_uuid) else None
def print: String =
build_uuid + " (platform: " + ml_platform + ", start: " + Build_Log.print_date(start) +