equal
deleted
inserted
replaced
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 " + |