# HG changeset patch
# User wenzelm
# Date 1493628946 -7200
# Node ID c266f045258bc13b98e5f20e67e545157e00ab89
# Parent  1b84d4109215269f4afa036238b079d8521ec09c
tuned;

diff -r 1b84d4109215 -r c266f045258b src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Mon May 01 10:05:02 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 10:55:46 2017 +0200
@@ -46,7 +46,9 @@
     session_logs: List[(String, String, URL)])
   {
     val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
-    val log_filename: Path = Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
+
+    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))