--- 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 =>
--- 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