# HG changeset patch
# User wenzelm
# Date 1494330168 -7200
# Node ID 3f5ebf9f380e52cf78cfd34d2b4a20a419129019
# Parent  84a0ac8a046ef1ba6c7e870dc1cf7621685d2e3d
clarified order of output;

diff -r 84a0ac8a046e -r 3f5ebf9f380e src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Tue May 09 11:29:18 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Tue May 09 13:42:48 2017 +0200
@@ -54,7 +54,7 @@
 
   val build_status_profiles: List[Build_Status.Profile] =
     build_log_jobs.map(job_name =>
-      Build_Status.Profile("Jenkins " + job_name,
+      Build_Status.Profile("jenkins " + job_name,
         Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
         Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
         Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))