# HG changeset patch
# User wenzelm
# Date 1699114762 -3600
# Node ID 6874791b24d929be870e47f96213bc9d7cd71426
# Parent  9f7a941176663d0ce6ca8eb095e18923d16bb032
tuned signature;

diff -r 9f7a94117666 -r 6874791b24d9 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 17:29:49 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 17:19:22 2023 +0100
@@ -195,7 +195,7 @@
 
       val store = Build_Log.store(options)
       using(store.open_database()) { db =>
-        def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = {
+        def pick_recent(days: Int, gap: Int): Option[(String, Option[String])] = {
           val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
           def runs = unknown_runs(items).filter(run => run.length >= gap)
 
@@ -210,9 +210,9 @@
           else runs.flatten.headOption.map(_.versions)
         }
 
-        pick_days(options.int("build_log_history") max history, 2) orElse
-        pick_days(200, 5) orElse
-        pick_days(2000, 1)
+        pick_recent(options.int("build_log_history") max history, 2) orElse
+        pick_recent(200, 5) orElse
+        pick_recent(2000, 1)
       }
     }