src/Pure/Admin/jenkins.scala
changeset 66880 486f4af28db9
parent 65935 73c099fa96a4
child 67008 eed58245b579
equal deleted inserted replaced
66879:593053cac3be 66880:486f4af28db9
    52 
    52 
    53   val build_log_jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
    53   val build_log_jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
    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, 0,
    57       Build_Status.Profile("jenkins " + job_name,
    58         Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
    58         sql =
    59         Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
    59           Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
    60         Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
    60           Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
    61         " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
    61           Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
       
    62           " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
    62 
    63 
    63 
    64 
    64   /* job info */
    65   /* job info */
    65 
    66 
    66   sealed case class Job_Info(
    67   sealed case class Job_Info(