proper result for rev == "";
authorwenzelm
Fri May 12 16:21:13 2017 +0200 (2017-05-12)
changeset 65808cb3e9d7f1d5f
parent 65807 a830c6257393
child 65809 8d5ac49388ea
proper result for rev == "";
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:11:59 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:21:13 2017 +0200
     1.3 @@ -125,19 +125,21 @@
     1.4        {
     1.5          val days = options.int("build_log_history") max history
     1.6          val items = recent_items(db, days = days, rev = rev, sql = sql)
     1.7 +        def runs = unknown_runs(items)
     1.8  
     1.9          val known_rev =
    1.10            rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
    1.11  
    1.12          if (history > 0 || known_rev) {
    1.13            val longest_run =
    1.14 -            (List.empty[Item] /: unknown_runs(items))({ case (item1, item2) =>
    1.15 +            (List.empty[Item] /: runs)({ case (item1, item2) =>
    1.16                if (item1.length >= item2.length) item1 else item2
    1.17              })
    1.18            if (longest_run.isEmpty) None
    1.19            else Some(longest_run(longest_run.length / 2).isabelle_version)
    1.20          }
    1.21 -        else Some(rev)
    1.22 +        else if (rev != "") Some(rev)
    1.23 +        else runs.flatten.headOption.map(_.isabelle_version)
    1.24        })
    1.25      }
    1.26    }