# HG changeset patch
# User wenzelm
# Date 1495617443 -7200
# Node ID 49f61e2f5a023d87ab90a1e5937abef6990fe0a4
# Parent  9584653df458b2e0106211b60977e3bf62105639
proper index;

diff -r 9584653df458 -r 49f61e2f5a02 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue May 23 21:31:33 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed May 24 11:17:23 2017 +0200
@@ -219,9 +219,8 @@
           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
   }
 
-  private def remote_build_history(arg: (String, Int), r: Remote_Build): Logger_Task =
+  private def remote_build_history(rev: String, i: Int, r: Remote_Build): Logger_Task =
   {
-    val (rev, index) = arg
     val task_name = "build_history-" + r.host
     Logger_Task(task_name, logger =>
       {
@@ -240,7 +239,7 @@
                   push_isabelle_home = push_isabelle_home,
                   options =
                     "-r " + Bash.string(rev) +
-                    " -N " + Bash.string(task_name) + "_" + (index + 1).toString +
+                    " -N " + Bash.string(task_name) + "_" + (if (i < 0) "" else (i + 1).toString) +
                     " -f " + r.options,
                   args = "-o timeout=10800 " + r.args)
 
@@ -402,9 +401,11 @@
         run_now(
           SEQ(List(build_release, build_history_base,
             PAR(remote_builds.map(seq =>
-              SEQ(seq.flatMap(r =>
-                r.pick(logger.options, rev, r.history_base_filter(hg)).zipWithIndex.
-                  map(remote_build_history(_, r)))))),
+              SEQ(
+                for {
+                  (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
+                  rev <- r.pick(logger.options, rev, r.history_base_filter(hg))
+                } yield remote_build_history(rev, i, r)))),
             Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
             Logger_Task("build_log_database",
               logger => Isabelle_Devel.build_log_database(logger.options)),