tuned output;
authorwenzelm
Sun May 07 17:06:05 2017 +0200 (2017-05-07)
changeset 65757a6522bb9acfa
parent 65756 2c6b5dd59db3
child 65758 d79126bb5d07
tuned output;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 16:42:36 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 17:06:05 2017 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  {
     1.5    private val default_target_dir = Path.explode("build_status")
     1.6    private val default_history_length = 30
     1.7 -  private val default_image_size = (800, 600)
     1.8 +  private val default_image_size = (640, 480)
     1.9  
    1.10  
    1.11    /* data profiles */
    1.12 @@ -230,9 +230,9 @@
    1.13                HTML.par(
    1.14                  List(
    1.15                    HTML.itemize(List(
    1.16 -                    HTML.bold(HTML.text("last timing: ")) ::
    1.17 +                    HTML.bold(HTML.text("timing: ")) ::
    1.18                        HTML.text(entries.head.timing.message_resources),
    1.19 -                    HTML.bold(HTML.text("last ML timing: ")) ::
    1.20 +                    HTML.bold(HTML.text("ML timing: ")) ::
    1.21                        HTML.text(entries.head.ml_timing.message_resources))),
    1.22                    HTML.image(name + ".png")))) })))
    1.23      }