src/Pure/Admin/jenkins.scala
changeset 65654 0fbaa9286331
parent 65653 f433c0e73307
child 65655 1b84d4109215
--- a/src/Pure/Admin/jenkins.scala	Mon May 01 09:49:22 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 09:52:11 2017 +0200
@@ -75,7 +75,7 @@
     }
   }
 
-  def build_job_builds(job_name: String): List[Job_Info] =
+  def build_job_infos(job_name: String): List[Job_Info] =
   {
     val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")