src/Pure/Admin/build_status.scala
2017-05-10 wenzelm 2017-05-10 stretch image according to history length;
2017-05-10 wenzelm 2017-05-10 actually plot extended profile history;
2017-05-09 wenzelm 2017-05-09 more output;
2017-05-09 wenzelm 2017-05-09 clarified;
2017-05-09 wenzelm 2017-05-09 tuned output;
2017-05-09 wenzelm 2017-05-09 more output;
2017-05-09 wenzelm 2017-05-09 tuned;
2017-05-09 wenzelm 2017-05-09 tuned;
2017-05-09 wenzelm 2017-05-09 tuned signature;
2017-05-08 wenzelm 2017-05-08 tuned message;
2017-05-08 wenzelm 2017-05-08 simplified default;
2017-05-08 wenzelm 2017-05-08 clarified image size;
2017-05-08 wenzelm 2017-05-08 plot heap size;
2017-05-08 wenzelm 2017-05-08 more specific workaround (see also ed7b5cd3a7f2);
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;