# HG changeset patch
# User wenzelm
# Date 1475348339 -7200
# Node ID 6ba87450894db98c7c6d5806db805d891a6e646b
# Parent  db9259a5e20eb9af0c302abef6394ae8c8d504b9
tuned messages -- facilitate copy-paste;

diff -r db9259a5e20e -r 6ba87450894d src/Pure/Tools/build_stats.scala
--- 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)