src/Pure/Admin/build_status.scala
Fri, 02 Mar 2018 20:46:25 +0100 wenzelm proper order;
Thu, 01 Mar 2018 20:44:38 +0100 wenzelm clarified date for presentation vs. formal pull_date;
Thu, 01 Mar 2018 20:18:24 +0100 wenzelm reveal raw data in CSV format;
Sat, 04 Nov 2017 15:24:40 +0100 wenzelm more robust sorted_entries;
Sat, 04 Nov 2017 14:41:26 +0100 wenzelm more convenient build_log_history;
Wed, 01 Nov 2017 18:24:39 +0100 wenzelm proper order for entries from multiple profiles, notably "AFP";
Wed, 01 Nov 2017 17:29:14 +0100 wenzelm tuned output;
Wed, 18 Oct 2017 20:26:32 +0200 wenzelm clarified output;
Wed, 18 Oct 2017 20:14:57 +0200 wenzelm tuned output;
Wed, 18 Oct 2017 19:53:19 +0200 wenzelm more thorough treatment of afp_version and afp_pull_date;
Fri, 07 Jul 2017 16:57:50 +0200 wenzelm proper check wrt. distinct entry dates;
Thu, 01 Jun 2017 15:19:50 +0200 wenzelm tuned signature;
Sat, 27 May 2017 13:01:25 +0200 wenzelm tuned signature;
Sat, 27 May 2017 12:57:57 +0200 wenzelm tuned signature;
Sat, 27 May 2017 12:52:36 +0200 wenzelm tuned signature;
Sat, 27 May 2017 12:36:27 +0200 wenzelm tuned signature;
Sat, 27 May 2017 12:33:14 +0200 wenzelm clarified signature;
Sat, 27 May 2017 00:30:48 +0200 wenzelm tuned layout;
Fri, 26 May 2017 23:33:42 +0200 wenzelm show errors from build_log database;
Fri, 26 May 2017 23:21:50 +0200 wenzelm support for message underline and tooltips;
Sun, 21 May 2017 23:41:46 +0200 wenzelm more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);
Sun, 21 May 2017 23:07:20 +0200 wenzelm show failed sessions on main page;
Thu, 18 May 2017 14:41:40 +0200 wenzelm tuned;
Thu, 18 May 2017 14:41:20 +0200 wenzelm more charts;
Thu, 18 May 2017 14:38:09 +0200 wenzelm uniform heap_scale;
Thu, 18 May 2017 14:14:20 +0200 wenzelm more plots from ml_statistics;
Thu, 18 May 2017 11:42:16 +0200 wenzelm tuned signature;
Wed, 17 May 2017 23:13:56 +0200 wenzelm do not store bulky ml_statistics;
Wed, 17 May 2017 23:05:30 +0200 wenzelm more output;
Wed, 17 May 2017 22:32:48 +0200 wenzelm plot average heap size;
Wed, 17 May 2017 21:24:16 +0200 wenzelm clarified use of XML.Cache;
Wed, 17 May 2017 14:58:48 +0200 wenzelm include full ML statistics: max heap size;
Wed, 17 May 2017 11:12:19 +0200 wenzelm proper order for entry list cons;
Wed, 17 May 2017 10:49:19 +0200 wenzelm proper check (amending ad35427dbe88);
Tue, 16 May 2017 22:57:12 +0200 wenzelm less restrictive filter: omit empty charts, but show latest timing;
Sun, 14 May 2017 22:04:52 +0200 wenzelm tuned signature;
Sun, 14 May 2017 21:54:35 +0200 wenzelm more systematic HTML.init_dir with css;
Sun, 14 May 2017 21:34:36 +0200 wenzelm prefer logical markup;
Fri, 12 May 2017 11:56:41 +0200 wenzelm tuned;
Wed, 10 May 2017 19:02:06 +0200 wenzelm stretch image according to history length;
Wed, 10 May 2017 17:24:31 +0200 wenzelm actually plot extended profile history;
Tue, 09 May 2017 21:43:46 +0200 wenzelm more output;
Tue, 09 May 2017 21:27:34 +0200 wenzelm clarified;
Tue, 09 May 2017 21:25:32 +0200 wenzelm tuned output;
Tue, 09 May 2017 20:36:34 +0200 wenzelm more output;
Tue, 09 May 2017 20:02:31 +0200 wenzelm tuned;
Tue, 09 May 2017 11:29:18 +0200 wenzelm tuned;
Tue, 09 May 2017 11:21:42 +0200 wenzelm tuned signature;
Mon, 08 May 2017 22:31:54 +0200 wenzelm tuned message;
Mon, 08 May 2017 21:58:15 +0200 wenzelm simplified default;
Mon, 08 May 2017 14:30:59 +0200 wenzelm clarified image size;
Mon, 08 May 2017 11:33:04 +0200 wenzelm plot heap size;
Mon, 08 May 2017 10:23:12 +0200 wenzelm more specific workaround (see also ed7b5cd3a7f2);
Sun, 07 May 2017 23:57:20 +0200 wenzelm cpu time is somewhat redundant for threads=1;
Sun, 07 May 2017 23:18:23 +0200 wenzelm clarified description vs. file name;
Sun, 07 May 2017 22:10:48 +0200 wenzelm tuned output;
Sun, 07 May 2017 21:42:23 +0200 wenzelm clarified types;
Sun, 07 May 2017 17:40:41 +0200 wenzelm more uniform charts;
Sun, 07 May 2017 17:29:38 +0200 wenzelm always show ml_timing -- in another chart;
Sun, 07 May 2017 17:10:03 +0200 wenzelm removed threshold: redundant due to sorting;
less more (0) -60 tip