--- 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,