src/Pure/Admin/build_stats.scala
changeset 65659 293141fb093d
parent 65658 be817b7b8354
child 65661 caec15e7c3eb
equal deleted inserted replaced
65658:be817b7b8354 65659:293141fb093d
    22     size: (Int, Int) = default_size,
    22     size: (Int, Int) = default_size,
    23     only_sessions: Set[String] = default_only_sessions,
    23     only_sessions: Set[String] = default_only_sessions,
    24     elapsed_threshold: Time = default_elapsed_threshold,
    24     elapsed_threshold: Time = default_elapsed_threshold,
    25     ml_timing: Option[Boolean] = default_ml_timing): List[String] =
    25     ml_timing: Option[Boolean] = default_ml_timing): List[String] =
    26   {
    26   {
    27     val job_infos = Jenkins.build_job_infos(job).sortBy(_.timestamp).reverse.take(history_length)
    27     val job_infos = Jenkins.build_job_infos(job).take(history_length)
    28     if (job_infos.isEmpty) error("No build infos for job " + quote(job))
    28     if (job_infos.isEmpty) error("No build infos for job " + quote(job))
    29 
    29 
    30     val all_infos =
    30     val all_infos =
    31       Par_List.map((job_info: Jenkins.Job_Info) =>
    31       Par_List.map((job_info: Jenkins.Job_Info) =>
    32         (job_info.timestamp / 1000, job_info.read_log_file.parse_build_info()), job_infos)
    32         (job_info.timestamp / 1000, job_info.read_log_file.parse_build_info()), job_infos)