# 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 {