src/Pure/Admin/jenkins.scala
changeset 65767 222ed8901008
parent 65764 1af6d544c2a3
child 65787 3f5ebf9f380e
equal deleted inserted replaced
65766:2edb89630a80 65767:222ed8901008
    54 
    54 
    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,
    57       Build_Status.Profile("Jenkins " + job_name,
    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.log_name + " LIKE " + SQL.string("%" + job_name)))
    60         Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
    60 
    61 
    61 
    62 
    62   /* job info */
    63   /* job info */
    63 
    64