more convenient build_log_history;
authorwenzelm
Sat Nov 04 14:41:26 2017 +0100 (12 months ago)
changeset 67002e8d64340d58b
parent 67001 b34fbf33a7ea
child 67003 49850a679c2c
more convenient build_log_history;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat Nov 04 12:39:25 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat Nov 04 14:41:26 2017 +0100
     1.3 @@ -487,6 +487,7 @@
     1.4      -D DIR       target directory (default """ + default_target_dir + """)
     1.5      -M           include full ML statistics
     1.6      -S SESSIONS  only given SESSIONS (comma separated)
     1.7 +    -l DAYS      length of relevant history (default """ + options.int("build_log_history") + """)
     1.8      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     1.9      -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
    1.10      -v           verbose
    1.11 @@ -498,6 +499,7 @@
    1.12          "D:" -> (arg => target_dir = Path.explode(arg)),
    1.13          "M" -> (_ => ml_statistics = true),
    1.14          "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
    1.15 +        "l:" -> (arg => options = options + ("build_log_history=" + arg)),
    1.16          "o:" -> (arg => options = options + arg),
    1.17          "s:" -> (arg =>
    1.18            space_explode('x', arg).map(Value.Int.parse(_)) match {