src/Pure/Admin/build_status.scala
2017-05-07 wenzelm 2017-05-07 cpu time is somewhat redundant for threads=1; tuned output;
2017-05-07 wenzelm 2017-05-07 clarified description vs. file name;
2017-05-07 wenzelm 2017-05-07 tuned output;
2017-05-07 wenzelm 2017-05-07 clarified types;
2017-05-07 wenzelm 2017-05-07 more uniform charts; tuned headings;
2017-05-07 wenzelm 2017-05-07 always show ml_timing -- in another chart;
2017-05-07 wenzelm 2017-05-07 removed threshold: redundant due to sorting;
2017-05-07 wenzelm 2017-05-07 tuned output;
2017-05-07 wenzelm 2017-05-07 parallel gnuplot invocation;
2017-05-07 wenzelm 2017-05-07 more HTML output;
2017-05-07 wenzelm 2017-05-07 clarified explicit Build_Status.Data operations; more HTML output;
2017-05-07 wenzelm 2017-05-07 more uniform threads value, notably for Pure session;
2017-05-07 wenzelm 2017-05-07 tuned;
2017-05-06 wenzelm 2017-05-06 added option verbose for SQL source;
2017-05-06 wenzelm 2017-05-06 tuned signature;
2017-05-06 wenzelm 2017-05-06 tuned;
2017-05-06 wenzelm 2017-05-06 clarified name;