more informative log_filename;
authorwenzelm
Mon, 01 May 2017 00:07:43 +0200
changeset 65652 349999526df3
parent 65651 2b78b7edf072
child 65653 f433c0e73307
more informative log_filename;
src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Sun Apr 30 23:41:08 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 00:07:43 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import java.net.URL
+import java.time.ZoneId
 
 import scala.util.matching.Regex
 
@@ -44,7 +45,11 @@
     output: URL,
     session_logs: List[(String, URL)])
   {
-    def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
+    def date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
+    def log_filename: Path =
+      Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
+    def read_main_log(): Build_Log.Log_File =
+      Build_Log.Log_File(log_filename.implode, Url.read(output))
     def read_session_log(name: String): Build_Log.Log_File =
       Build_Log.Log_File(name,
         session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")