src/Pure/Admin/build_status.scala
2017-05-27 wenzelm 2017-05-27 clarified signature;
2017-05-27 wenzelm 2017-05-27 tuned layout;
2017-05-26 wenzelm 2017-05-26 show errors from build_log database;
2017-05-26 wenzelm 2017-05-26 support for message underline and tooltips;
2017-05-21 wenzelm 2017-05-21 more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);
2017-05-21 wenzelm 2017-05-21 show failed sessions on main page;
2017-05-18 wenzelm 2017-05-18 tuned;
2017-05-18 wenzelm 2017-05-18 more charts;
2017-05-18 wenzelm 2017-05-18 uniform heap_scale; tuned;
2017-05-18 wenzelm 2017-05-18 more plots from ml_statistics;
2017-05-18 wenzelm 2017-05-18 tuned signature;
2017-05-17 wenzelm 2017-05-17 do not store bulky ml_statistics;
2017-05-17 wenzelm 2017-05-17 more output;
2017-05-17 wenzelm 2017-05-17 plot average heap size;
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;