src/Pure/Admin/jenkins.scala
changeset 65788 bc00ac4dba25
parent 65787 3f5ebf9f380e
child 65798 d459db0f6135
equal deleted inserted replaced
65787:3f5ebf9f380e 65788:bc00ac4dba25
    48   }
    48   }
    49 
    49 
    50 
    50 
    51   /* build log status */
    51   /* build log status */
    52 
    52 
    53   val build_log_jobs = List("isabelle-nightly-benchmark")
    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,
    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 " +