src/Pure/Admin/build_status.scala
2017-05-17 wenzelm 2017-05-17 clarified use of XML.Cache;
2017-05-17 wenzelm 2017-05-17 include full ML statistics: max heap size;
2017-05-17 wenzelm 2017-05-17 proper order for entry list cons;
2017-05-17 wenzelm 2017-05-17 proper check (amending ad35427dbe88);
2017-05-16 wenzelm 2017-05-16 less restrictive filter: omit empty charts, but show latest timing;
2017-05-14 wenzelm 2017-05-14 tuned signature;
2017-05-14 wenzelm 2017-05-14 more systematic HTML.init_dir with css;
2017-05-14 wenzelm 2017-05-14 prefer logical markup;
2017-05-12 wenzelm 2017-05-12 tuned;
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;