more parallelism;
authorwenzelm
Mon, 01 May 2017 11:24:41 +0200
changeset 65662 3db6a13fdffd
parent 65661 caec15e7c3eb
child 65663 61cd86bb9613
more parallelism;
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)
   }