src/Pure/Tools/build_stats.scala
changeset 63984 6ba87450894d
parent 63926 70973a1b4ec0
child 64054 1fc9ab31720d
equal deleted inserted replaced
63983:db9259a5e20e 63984:6ba87450894d
   218       val jobs = getopts(args)
   218       val jobs = getopts(args)
   219       val all_jobs = CI_API.build_jobs()
   219       val all_jobs = CI_API.build_jobs()
   220       val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
   220       val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
   221 
   221 
   222       if (jobs.isEmpty)
   222       if (jobs.isEmpty)
   223         error("No build jobs given. Available jobs: " + commas(all_jobs))
   223         error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
   224 
   224 
   225       if (bad_jobs.nonEmpty)
   225       if (bad_jobs.nonEmpty)
   226         error("Unknown build jobs: " + commas(bad_jobs) +
   226         error("Unknown build jobs: " + bad_jobs.mkString(" ") +
   227           "\nAvailable jobs: " + commas(all_jobs.sorted))
   227           "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
   228 
   228 
   229       for (job <- jobs) {
   229       for (job <- jobs) {
   230         val dir = target_dir + Path.basic(job)
   230         val dir = target_dir + Path.basic(job)
   231         Output.writeln(dir.implode)
   231         Output.writeln(dir.implode)
   232         val sessions =
   232         val sessions =