# HG changeset patch
# User wenzelm
# Date 1701001971 -3600
# Node ID 0da44db32646dc2aa1add8f4fe200e5dd25c95a2
# Parent  07799c394b6d37b9b24f7c9418bda0259e732b67
tuned whitespace;

diff -r 07799c394b6d -r 0da44db32646 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 25 20:47:33 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 26 13:32:51 2023 +0100
@@ -162,14 +162,12 @@
     }
 
     def pick(options: Options): Option[(String, Option[String])] = {
-
       val store = Build_Log.store(options)
       using(store.open_database()) { db =>
         def get(days: Int, gap: Int): Option[(String, Option[String])] = {
           val runs = history(db, days = days).unknown_runs(filter = run => run.length >= gap)
           Build_Log.History.Run.longest(runs).median.map(_.versions)
         }
-
         get(options.int("build_log_history") max history, 2) orElse
         get(300, 8) orElse
         get(3000, 32) orElse