# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1664522845 -7200
# Node ID fb2be77a7819e77630d6e327471ec908af7dfdcb
# Parent  64e8d4afcf1075fa2601dda97448c1ee4eb244ae
tweaked;

diff -r 64e8d4afcf10 -r fb2be77a7819 src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Thu Sep 29 14:03:40 2022 +0000
+++ b/src/Pure/Admin/ci_build.scala	Fri Sep 30 09:27:25 2022 +0200
@@ -64,11 +64,11 @@
     cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description))
 
   def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse
-    error("Unknown job" + quote(name))
+    error("Unknown job " + quote(name))
 
   val timing =
     Job(
-      "timing", "runs benchmark and timing sessions",
+      "benchmark", "runs benchmark and timing sessions",
       Profile(threads = 6, jobs = 1, numa = false),
       Build_Config(
         documents = false,