# HG changeset patch
# User wenzelm
# Date 1493630432 -7200
# Node ID caec15e7c3ebfff39f8ebb3ea35d5f1b39075037
# Parent  dfecaf0fc0696048df820ff49f279454623ea716
tuned;

diff -r dfecaf0fc069 -r caec15e7c3eb src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Mon May 01 11:12:46 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala	Mon May 01 11:20:32 2017 +0200
@@ -28,8 +28,12 @@
     if (job_infos.isEmpty) error("No build infos for job " + quote(job))
 
     val all_infos =
-      Par_List.map((job_info: Jenkins.Job_Info) =>
-        (job_info.timestamp / 1000, job_info.read_log_file.parse_build_info()), job_infos)
+      Par_List.map((info: Jenkins.Job_Info) =>
+        {
+          val t = info.timestamp / 1000
+          val log_file = Build_Log.Log_File(info.log_filename.implode, Url.read(info.main_log))
+          (t, log_file.parse_build_info())
+        }, job_infos)
     val all_sessions =
       (Set.empty[String] /: all_infos)(
         { case (s, (_, info)) => s ++ info.sessions.keySet })
diff -r dfecaf0fc069 -r caec15e7c3eb src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Mon May 01 11:12:46 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 11:20:32 2017 +0200
@@ -63,9 +63,6 @@
     def log_filename: Path =
       Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
 
-    def read_log_file(): Build_Log.Log_File =
-      Build_Log.Log_File(log_filename.implode, Url.read(main_log))
-
     def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] =
     {
       def get_log(ext: String): Option[URL] =