diff -r f433c0e73307 -r 0fbaa9286331 src/Pure/Admin/jenkins.scala
--- 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)$""")