# HG changeset patch
# User wenzelm
# Date 1493625131 -7200
# Node ID 0fbaa92863310d5df8dbc9a1adbdae1ad63d68c4
# Parent  f433c0e7330721ff33aed25cfac35d9810acb665
tuned signature;

diff -r f433c0e73307 -r 0fbaa9286331 src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Mon May 01 09:49:22 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala	Mon May 01 09:52:11 2017 +0200
@@ -24,7 +24,7 @@
     elapsed_threshold: Time = default_elapsed_threshold,
     ml_timing: Option[Boolean] = default_ml_timing): List[String] =
   {
-    val job_infos = Jenkins.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
+    val job_infos = Jenkins.build_job_infos(job).sortBy(_.timestamp).reverse.take(history_length)
     if (job_infos.isEmpty) error("No build infos for job " + quote(job))
 
     val all_infos =
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)$""")