# HG changeset patch
# User wenzelm
# Date 1493590063 -7200
# Node ID 349999526df3b1c4316c9f78036f8aebedaf5736
# Parent  2b78b7edf0722d323f4c28273801619d3525f89f
more informative log_filename;

diff -r 2b78b7edf072 -r 349999526df3 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 "")