# HG changeset patch
# User wenzelm
# Date 1692699511 -7200
# Node ID 05de3e06831249f6fc33f9a479fb63a9311e866c
# Parent  8ba186dc9bc87dd64fc6ebdb302b339614edc829
proper sync_database for receive timeout;

diff -r 8ba186dc9bc8 -r 05de3e068312 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Aug 22 11:54:06 2023 +0200
+++ b/src/Pure/System/progress.scala	Tue Aug 22 12:18:31 2023 +0200
@@ -343,7 +343,11 @@
 
     _consumer = Consumer_Thread.fork_bulk[Progress.Output](name = "Database_Progress.consumer")(
       bulk = _ => true, timeout = timeout,
-      consume = bulk_output => (bulk_output.grouped(200).toList.flatMap(consume), true))
+      consume = { bulk_output =>
+        val results =
+          if (bulk_output.isEmpty) consume(Nil)
+          else bulk_output.grouped(200).toList.flatMap(consume)
+        (results, true) })
   }
 
   def exit(close: Boolean = false): Unit = synchronized {