src/Pure/Admin/jenkins.scala
changeset 65656 c266f045258b
parent 65655 1b84d4109215
child 65657 2773b6859c55
--- 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))