--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Nov 02 21:35:04 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Nov 03 10:12:34 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 =>