--- 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 })
--- 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] =