--- a/src/Pure/Build/build_process.scala Sun Mar 10 18:01:14 2024 +0100
+++ b/src/Pure/Build/build_process.scala Sun Mar 10 22:42:27 2024 +0100
@@ -928,9 +928,10 @@
update_sessions(db, state.sessions, old_state.sessions),
update_pending(db, state.pending, old_state.pending),
update_running(db, state.running, old_state.running),
- update_results(db, state.results, old_state.results))
+ update_results(db, state.results, old_state.results)
+ ).filter(_.defined)
- if (updates.exists(_.defined)) {
+ if (updates.nonEmpty) {
val serial = state.next_serial
write_updates(db, build_id, serial, updates)
stamp_worker(db, worker_uuid, serial)