# HG changeset patch
# User wenzelm
# Date 1493630681 -7200
# Node ID 3db6a13fdffdad186ecbd6468d8c7bc958dc664e
# Parent  caec15e7c3ebfff39f8ebb3ea35d5f1b39075037
more parallelism;

diff -r caec15e7c3eb -r 3db6a13fdffd src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Mon May 01 11:20:32 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 11:24:41 2017 +0200
@@ -43,10 +43,8 @@
   def download_logs(job_names: List[String], dir: Path, progress: Progress = No_Progress)
   {
     val store = Sessions.store()
-    for {
-      job_name <- job_names.iterator
-      info <- build_job_infos(job_name).iterator
-    } info.download_log(store, dir, progress)
+    val infos = job_names.flatMap(build_job_infos(_))
+    Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
   }