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