merged
authorwenzelm
Fri, 03 Nov 2023 10:13:41 +0100
changeset 78886 b82c2f801f2c
parent 78884 0233d5a5a4ca (current diff)
parent 78885 9d0faaa77e5d (diff)
child 78887 6996a20a1b7c
child 78888 95bbf9a576b3
merged
--- 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 =>