# HG changeset patch
# User wenzelm
# Date 1496669871 -7200
# Node ID 6706d6f0afda1667dff71671b3a627429eef70ba
# Parent  cec184536dfdd10ad5f3e805dddce0a30fe09329
cover more history;

diff -r cec184536dfd -r 6706d6f0afda src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Jun 05 13:19:14 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon Jun 05 15:37:51 2017 +0200
@@ -133,12 +133,12 @@
       val store = Build_Log.store(options)
       using(store.open_database())(db =>
       {
-        def pick_days(days: Int): Option[String] =
+        def pick_days(days: Int, gap: Int): Option[String] =
         {
           val items =
             recent_items(db, days = days, rev = rev, sql = sql).
               filter(item => filter(item.isabelle_version))
-          def runs = unknown_runs(items)
+          def runs = unknown_runs(items).filter(run => run.length >= gap)
 
           val known_rev =
             rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
@@ -155,9 +155,9 @@
           else runs.flatten.headOption.map(_.isabelle_version)
         }
 
-        pick_days(options.int("build_log_history") max history) orElse
-        pick_days(200) orElse
-        pick_days(2000)
+        pick_days(options.int("build_log_history") max history, 2) orElse
+        pick_days(200, 5) orElse
+        pick_days(2000, 1)
       })
     }
   }