tuned signature;
authorwenzelm
Sun, 10 Mar 2024 11:51:56 +0100
changeset 79845 0158007dfdab
parent 79844 ac40138234ce
child 79846 3d83a2554a71
tuned signature;
src/Pure/Build/build.scala
src/Pure/Build/build_process.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) {
--- 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) +