# HG changeset patch
# User wenzelm
# Date 1699002821 -3600
# Node ID b82c2f801f2c5de21b2819bc3291c98dd3db5197
# Parent  0233d5a5a4caf0ea7af6c67b7228c459b0e0aabd# Parent  9d0faaa77e5d04ea3fde7669406d9b3eeefcbdac
merged

diff -r 0233d5a5a4ca -r b82c2f801f2c src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Nov 03 10:03:05 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Nov 03 10:13:41 2023 +0100
@@ -430,7 +430,8 @@
     rev: String,
     afp_rev: Option[String],
     i: Int,
-    r: Remote_Build
+    r: Remote_Build,
+    progress: Progress = new Progress
   ) : Logger_Task = {
     val task_name = "build_history-" + r.host
     Logger_Task(task_name,
@@ -461,7 +462,8 @@
               log_file
             }
 
-          Build_Log.build_log_database(logger.options, log_files, ml_statistics = true)
+          Build_Log.build_log_database(logger.options, log_files,
+            progress = progress, ml_statistics = true)
         }
       })
   }
@@ -653,7 +655,9 @@
                         (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
                       } yield () => {
                         r.pick(logger.options, hg.id(), history_base_filter(r))
-                          .map({ case (rev, afp_rev) => remote_build_history(rev, afp_rev, i, r) })
+                          .map({ case (rev, afp_rev) =>
+                            remote_build_history(rev, afp_rev, i, r,
+                              progress = build_log_database_progress) })
                       }
                     ))),
                   Logger_Task("build_status", logger =>