# HG changeset patch
# User wenzelm
# Date 1710106947 -3600
# Node ID 9cb5e20df9a4a2e48393c4c3f0a986ced7edd525
# Parent  15948836fa908bfc011e2f16e99ddfe51b7780c9
tuned;

diff -r 15948836fa90 -r 9cb5e20df9a4 src/Pure/Build/build_process.scala
--- 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)