# HG changeset patch
# User wenzelm
# Date 1494169565 -7200
# Node ID a6522bb9acfa7f88629cf85f6917428fc82a61a5
# Parent  2c6b5dd59db342a69a81e7f35251012a2bc13d4d
tuned output;

diff -r 2c6b5dd59db3 -r a6522bb9acfa src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 07 16:42:36 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 07 17:06:05 2017 +0200
@@ -11,7 +11,7 @@
 {
   private val default_target_dir = Path.explode("build_status")
   private val default_history_length = 30
-  private val default_image_size = (800, 600)
+  private val default_image_size = (640, 480)
 
 
   /* data profiles */
@@ -230,9 +230,9 @@
               HTML.par(
                 List(
                   HTML.itemize(List(
-                    HTML.bold(HTML.text("last timing: ")) ::
+                    HTML.bold(HTML.text("timing: ")) ::
                       HTML.text(entries.head.timing.message_resources),
-                    HTML.bold(HTML.text("last ML timing: ")) ::
+                    HTML.bold(HTML.text("ML timing: ")) ::
                       HTML.text(entries.head.ml_timing.message_resources))),
                   HTML.image(name + ".png")))) })))
     }