src/Pure/Admin/build_status.scala
17 months ago wenzelm 2017-11-01 proper order for entries from multiple profiles, notably "AFP";
17 months ago wenzelm 2017-11-01 tuned output;
18 months ago wenzelm 2017-10-18 clarified output;
18 months ago wenzelm 2017-10-18 tuned output;
18 months ago wenzelm 2017-10-18 more thorough treatment of afp_version and afp_pull_date;
21 months ago wenzelm 2017-07-07 proper check wrt. distinct entry dates;
23 months ago wenzelm 2017-06-01 tuned signature;
23 months ago wenzelm 2017-05-27 tuned signature;
23 months ago wenzelm 2017-05-27 tuned signature;
23 months ago wenzelm 2017-05-27 tuned signature;
23 months ago wenzelm 2017-05-27 tuned signature;
23 months ago wenzelm 2017-05-27 clarified signature;
23 months ago wenzelm 2017-05-27 tuned layout;
23 months ago wenzelm 2017-05-26 show errors from build_log database;
23 months ago wenzelm 2017-05-26 support for message underline and tooltips;
23 months ago wenzelm 2017-05-21 more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);
23 months ago wenzelm 2017-05-21 show failed sessions on main page;
23 months ago wenzelm 2017-05-18 tuned;
23 months ago wenzelm 2017-05-18 more charts;
23 months ago wenzelm 2017-05-18 uniform heap_scale; tuned;
23 months ago wenzelm 2017-05-18 more plots from ml_statistics;
23 months ago wenzelm 2017-05-18 tuned signature;
23 months ago wenzelm 2017-05-17 do not store bulky ml_statistics;
23 months ago wenzelm 2017-05-17 more output;
23 months ago wenzelm 2017-05-17 plot average heap size;
23 months ago wenzelm 2017-05-17 clarified use of XML.Cache;
23 months ago wenzelm 2017-05-17 include full ML statistics: max heap size;
23 months ago wenzelm 2017-05-17 proper order for entry list cons;
23 months ago wenzelm 2017-05-17 proper check (amending ad35427dbe88);
23 months ago wenzelm 2017-05-16 less restrictive filter: omit empty charts, but show latest timing;
23 months ago wenzelm 2017-05-14 tuned signature;
23 months ago wenzelm 2017-05-14 more systematic HTML.init_dir with css;
23 months ago wenzelm 2017-05-14 prefer logical markup;
23 months ago wenzelm 2017-05-12 tuned;
23 months ago wenzelm 2017-05-10 stretch image according to history length;
23 months ago wenzelm 2017-05-10 actually plot extended profile history;
23 months ago wenzelm 2017-05-09 more output;
23 months ago wenzelm 2017-05-09 clarified;
23 months ago wenzelm 2017-05-09 tuned output;
23 months ago wenzelm 2017-05-09 more output;
23 months ago wenzelm 2017-05-09 tuned;
23 months ago wenzelm 2017-05-09 tuned;
23 months ago wenzelm 2017-05-09 tuned signature;
23 months ago wenzelm 2017-05-08 tuned message;
23 months ago wenzelm 2017-05-08 simplified default;
23 months ago wenzelm 2017-05-08 clarified image size;
23 months ago wenzelm 2017-05-08 plot heap size;
23 months ago wenzelm 2017-05-08 more specific workaround (see also ed7b5cd3a7f2);
23 months ago wenzelm 2017-05-07 cpu time is somewhat redundant for threads=1; tuned output;
23 months ago wenzelm 2017-05-07 clarified description vs. file name;
23 months ago wenzelm 2017-05-07 tuned output;
23 months ago wenzelm 2017-05-07 clarified types;
23 months ago wenzelm 2017-05-07 more uniform charts; tuned headings;
23 months ago wenzelm 2017-05-07 always show ml_timing -- in another chart;
23 months ago wenzelm 2017-05-07 removed threshold: redundant due to sorting;
23 months ago wenzelm 2017-05-07 tuned output;
23 months ago wenzelm 2017-05-07 parallel gnuplot invocation;
23 months ago wenzelm 2017-05-07 more HTML output;
23 months ago wenzelm 2017-05-07 clarified explicit Build_Status.Data operations; more HTML output;
23 months ago wenzelm 2017-05-07 more uniform threads value, notably for Pure session;