equal
deleted
inserted
replaced
24 |
24 |
25 def generate(job: String): Unit = { |
25 def generate(job: String): Unit = { |
26 println(s"=== $job ===") |
26 println(s"=== $job ===") |
27 |
27 |
28 val dir = target_dir + Path.basic(job) |
28 val dir = target_dir + Path.basic(job) |
29 val sessions = Build_Stats.present_job(job, dir) |
29 val sessions = Build_Stats_Legacy.present_job(job, dir) |
30 |
30 |
31 val sections = |
31 val sections = |
32 cat_lines( |
32 cat_lines( |
33 sessions.map(session => |
33 sessions.map(session => |
34 "<p id=" + quote("session_" + HTML.output(session)) + ">" + |
34 "<p id=" + quote("session_" + HTML.output(session)) + ">" + |