src/Pure/Admin/jenkins.scala
changeset 65896 18f5014331a1
parent 65798 d459db0f6135
child 65935 73c099fa96a4
equal deleted inserted replaced
65895:744878d72021 65896:18f5014331a1
    55   val build_status_profiles: List[Build_Status.Profile] =
    55   val build_status_profiles: List[Build_Status.Profile] =
    56     build_log_jobs.map(job_name =>
    56     build_log_jobs.map(job_name =>
    57       Build_Status.Profile("jenkins " + job_name, 0,
    57       Build_Status.Profile("jenkins " + job_name, 0,
    58         Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
    58         Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
    59         Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
    59         Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
    60         Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
    60         Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
       
    61         " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
    61 
    62 
    62 
    63 
    63   /* job info */
    64   /* job info */
    64 
    65 
    65   sealed case class Job_Info(
    66   sealed case class Job_Info(