src/Pure/Admin/build_status.scala
changeset 65755 21b4bfa6d204
parent 65754 05c6a29c9132
child 65756 2c6b5dd59db3
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 16:14:49 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 16:31:39 2017 +0200
     1.3 @@ -225,9 +225,15 @@
     1.4                HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
     1.5            sessions.flatMap({ case (name, entries) =>
     1.6              List(
     1.7 -              HTML.section(name + " (" + entries.head.timing.message_resources + ")") +
     1.8 -                HTML.id("session_" + name),
     1.9 -              HTML.par(List(HTML.image(name + ".png")))) })))
    1.10 +              HTML.section(name) + HTML.id("session_" + name),
    1.11 +              HTML.par(
    1.12 +                List(
    1.13 +                  HTML.itemize(List(
    1.14 +                    HTML.bold(HTML.text("last timing: ")) ::
    1.15 +                      HTML.text(entries.head.timing.message_resources),
    1.16 +                    HTML.bold(HTML.text("last ML timing: ")) ::
    1.17 +                      HTML.text(entries.head.ml_timing.message_resources))),
    1.18 +                  HTML.image(name + ".png")))) })))
    1.19      }
    1.20  
    1.21      val heading = "Build status (" + data.date + ")"