--- a/src/Pure/Admin/build_status.scala Sun May 07 16:14:49 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sun May 07 16:31:39 2017 +0200
@@ -225,9 +225,15 @@
HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
sessions.flatMap({ case (name, entries) =>
List(
- HTML.section(name + " (" + entries.head.timing.message_resources + ")") +
- HTML.id("session_" + name),
- HTML.par(List(HTML.image(name + ".png")))) })))
+ HTML.section(name) + HTML.id("session_" + name),
+ HTML.par(
+ List(
+ HTML.itemize(List(
+ HTML.bold(HTML.text("last timing: ")) ::
+ HTML.text(entries.head.timing.message_resources),
+ HTML.bold(HTML.text("last ML timing: ")) ::
+ HTML.text(entries.head.ml_timing.message_resources))),
+ HTML.image(name + ".png")))) })))
}
val heading = "Build status (" + data.date + ")"