# HG changeset patch
# User wenzelm
# Date 1710067916 -3600
# Node ID 0158007dfdab6cf08933a7051205edf5222aaf76
# Parent  ac40138234ce4b169978331756a7d1c2fcbc2074
tuned signature;

diff -r ac40138234ce -r 0158007dfdab src/Pure/Build/build.scala
--- 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) {
diff -r ac40138234ce -r 0158007dfdab src/Pure/Build/build_process.scala
--- 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) +