# HG changeset patch
# User wenzelm
# Date 1494598873 -7200
# Node ID cb3e9d7f1d5f0bd4cb5903d1725c694ed469c59e
# Parent  a830c62573939a5802738f09f22d9c52c96d10d2
proper result for rev == "";

diff -r a830c6257393 -r cb3e9d7f1d5f 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)
       })
     }
   }