# HG changeset patch
# User wenzelm
# Date 1699112716 -3600
# Node ID 541ea53022006201290aa1a4ad4a6930a0eb4345
# Parent  3523df57df5158e517ed012f87edaeb12357025b
clarified signature;

diff -r 3523df57df51 -r 541ea5302200 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 16:31:02 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 16:45:16 2023 +0100
@@ -189,11 +189,8 @@
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
 
-    def pick(
-      options: Options,
-      rev: String = "",
-      filter: Item => Boolean = _ => true
-    ): Option[(String, Option[String])] = {
+    def pick(options: Options, filter: Item => Boolean): Option[(String, Option[String])] = {
+      val rev = get_rev()
       val afp_rev = if (afp) Some(get_afp_rev()) else None
 
       val store = Build_Log.store(options)
@@ -656,7 +653,7 @@
                       for {
                         (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
                       } yield () => {
-                        r.pick(logger.options, hg.id(), history_base_filter(r))
+                        r.pick(logger.options, history_base_filter(r))
                           .map({ case (rev, afp_rev) =>
                             remote_build_history(rev, afp_rev, i, r,
                               progress = build_log_database_progress) })