proper result for rev == "";
authorwenzelm
Fri, 12 May 2017 16:21:13 +0200
changeset 65808 cb3e9d7f1d5f
parent 65807 a830c6257393
child 65809 8d5ac49388ea
proper result for rev == "";
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:11:59 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:21:13 2017 +0200
@@ -125,19 +125,21 @@
       {
         val days = options.int("build_log_history") max history
         val items = recent_items(db, days = days, rev = rev, sql = sql)
+        def runs = unknown_runs(items)
 
         val known_rev =
           rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
 
         if (history > 0 || known_rev) {
           val longest_run =
-            (List.empty[Item] /: unknown_runs(items))({ case (item1, item2) =>
+            (List.empty[Item] /: runs)({ case (item1, item2) =>
               if (item1.length >= item2.length) item1 else item2
             })
           if (longest_run.isEmpty) None
           else Some(longest_run(longest_run.length / 2).isabelle_version)
         }
-        else Some(rev)
+        else if (rev != "") Some(rev)
+        else runs.flatten.headOption.map(_.isabelle_version)
       })
     }
   }