src/Pure/Tools/build_stats.scala
changeset 63984 6ba87450894d
parent 63926 70973a1b4ec0
child 64054 1fc9ab31720d
--- a/src/Pure/Tools/build_stats.scala	Sat Oct 01 20:03:17 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Sat Oct 01 20:58:59 2016 +0200
@@ -220,11 +220,11 @@
       val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
 
       if (jobs.isEmpty)
-        error("No build jobs given. Available jobs: " + commas(all_jobs))
+        error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
 
       if (bad_jobs.nonEmpty)
-        error("Unknown build jobs: " + commas(bad_jobs) +
-          "\nAvailable jobs: " + commas(all_jobs.sorted))
+        error("Unknown build jobs: " + bad_jobs.mkString(" ") +
+          "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
 
       for (job <- jobs) {
         val dir = target_dir + Path.basic(job)