Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Mon, 01 May 2017 09:52:11 +0200
changeset 65654 0fbaa9286331
parent 65653 f433c0e73307
child 65655 1b84d4109215
tuned signature;
src/Pure/Admin/build_stats.scala file | annotate | diff | comparison | revisions
src/Pure/Admin/jenkins.scala file | annotate | diff | comparison | revisions 
--- 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 =
--- 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)$""")
isabelle