# HG changeset patch
# User wenzelm
# Date 1687947362 -7200
# Node ID 5c91541284cd051cda855a45c9df1cf709d37c49
# Parent  60fa7a0b9372daf0a70d66aa7683e0664f34d142
show only active builds;

diff -r 60fa7a0b9372 -r 5c91541284cd src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jun 28 12:13:46 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jun 28 12:16:02 2023 +0200
@@ -383,7 +383,7 @@
 
   def read_builds(options: Options): List[Build_Process.Build] =
     using_option(Store(options).maybe_open_build_database(Build_Process.Data.database))(
-      Build_Process.read_builds).getOrElse(Nil)
+      Build_Process.read_builds).getOrElse(Nil).filter(_.active)
 
   def print_builds(options: Options, builds: List[Build_Process.Build]): String =
     using_optional(Store(options).maybe_open_build_database(Build_Process.Data.database)) { build_database =>
diff -r 60fa7a0b9372 -r 5c91541284cd src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jun 28 12:13:46 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jun 28 12:16:02 2023 +0200
@@ -148,7 +148,9 @@
     options: String,
     start: Date,
     stop: Option[Date]
-  )
+  ) {
+    def active: Boolean = stop.isEmpty
+  }
 
   case class Worker(
     worker_uuid: String,  // Database_Progress.agent_uuid