# HG changeset patch
# User wenzelm
# Date 1692610936 -7200
# Node ID 6cdf9b00dc767fd01bfae6351734fe6c65ace014
# Parent  7f564f33172b3c1d78bb08c863f51806092b7533
tuned;

diff -r 7f564f33172b -r 6cdf9b00dc76 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Mon Aug 21 11:24:47 2023 +0200
+++ b/src/Pure/System/progress.scala	Mon Aug 21 11:42:16 2023 +0200
@@ -328,9 +328,7 @@
       consume = { bulk_output0 =>
         val results =
           for (bulk_output <- bulk_output0.grouped(200).toList) yield {
-            val serial = _serial
             val serial_db = Progress.private_data.read_messages_serial(db, _context)
-
             _serial = _serial max serial_db
 
             if (bulk_output.nonEmpty) {
@@ -347,13 +345,10 @@
                   yield (_serial + i + 1) -> out.message
 
               Progress.private_data.write_messages(db, _context, messages)
-
               _serial = messages.last._1
             }
 
-            if (_serial != serial_db) {
-              Progress.private_data.update_agent(db, _agent_uuid, _serial)
-            }
+            if (_serial != serial_db) Progress.private_data.update_agent(db, _agent_uuid, _serial)
 
             bulk_output.map(_ => Exn.Res(()))
           }