# HG changeset patch # User wenzelm # Date 1494022984 -7200 # Node ID 0729c09be90cbbb58f243fa321e00ec15eb1530a # Parent 2e7230b66a32ecc727579d742a575284f254fa40 tuned messages; diff -r 2e7230b66a32 -r 0729c09be90c src/Pure/Admin/build_stats.scala --- a/src/Pure/Admin/build_stats.scala Sat May 06 00:12:46 2017 +0200 +++ b/src/Pure/Admin/build_stats.scala Sat May 06 00:23:04 2017 +0200 @@ -63,7 +63,7 @@ using(store.open_database())(db => { for (profile <- profiles) { - progress.echo("database query " + profile.name) + progress.echo("database query " + quote(profile.name)) val columns = List( Build_Log.Data.pull_date, @@ -236,14 +236,14 @@ Usage: isabelle build_stats [OPTIONS] Options are: - -D DIR target directory (default " + default_target_dir + ") + -D DIR target directory (default """ + default_target_dir + """) -M only ML timing -S SESSIONS only given SESSIONS (comma separated) -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes) - -l LENGTH length of history (default 100) + -l LENGTH length of history (default """ + default_history_length + """) -m include ML timing -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -s WxH size of PNG image (default 800x600) + -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) Present performance statistics from build log database, which is specified via system options build_log_database_host, build_log_database_user etc.