tuned messages -- facilitate copy-paste;
authorwenzelm
Sat, 01 Oct 2016 20:58:59 +0200
changeset 63984 6ba87450894d
parent 63983 db9259a5e20e
child 63985 4effb93c2a09
tuned messages -- facilitate copy-paste;
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)