equal
deleted
inserted
replaced
62 |
62 |
63 def show_jobs: String = |
63 def show_jobs: String = |
64 cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description)) |
64 cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description)) |
65 |
65 |
66 def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse |
66 def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse |
67 error("Unknown job" + quote(name)) |
67 error("Unknown job " + quote(name)) |
68 |
68 |
69 val timing = |
69 val timing = |
70 Job( |
70 Job( |
71 "timing", "runs benchmark and timing sessions", |
71 "benchmark", "runs benchmark and timing sessions", |
72 Profile(threads = 6, jobs = 1, numa = false), |
72 Profile(threads = 6, jobs = 1, numa = false), |
73 Build_Config( |
73 Build_Config( |
74 documents = false, |
74 documents = false, |
75 select = List( |
75 select = List( |
76 Path.explode("$ISABELLE_HOME/src/Benchmarks")), |
76 Path.explode("$ISABELLE_HOME/src/Benchmarks")), |