# HG changeset patch
# User wenzelm
# Date 1509802886 -3600
# Node ID e8d64340d58bafd34d84d4a22df88234164197cb
# Parent  b34fbf33a7ea27d8c5f568671316eec3f9525396
more convenient build_log_history;

diff -r b34fbf33a7ea -r e8d64340d58b src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Nov 04 12:39:25 2017 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Nov 04 14:41:26 2017 +0100
@@ -487,6 +487,7 @@
     -D DIR       target directory (default """ + default_target_dir + """)
     -M           include full ML statistics
     -S SESSIONS  only given SESSIONS (comma separated)
+    -l DAYS      length of relevant history (default """ + options.int("build_log_history") + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
     -v           verbose
@@ -498,6 +499,7 @@
         "D:" -> (arg => target_dir = Path.explode(arg)),
         "M" -> (_ => ml_statistics = true),
         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
+        "l:" -> (arg => options = options + ("build_log_history=" + arg)),
         "o:" -> (arg => options = options + arg),
         "s:" -> (arg =>
           space_explode('x', arg).map(Value.Int.parse(_)) match {