| Thu, 28 Mar 2024 16:27:36 +0100 |
wenzelm |
clarified modules: more official Sessions.notable_groups;
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 20:41:18 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 20 Nov 2023 14:11:34 +0100 |
wenzelm |
suppress duplicate entries systematically using log_name: e.g. relevant for AFP;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 19:29:19 +0100 |
wenzelm |
clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 19:31:22 +0100 |
wenzelm |
avoid duplicate data;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 19:14:59 +0100 |
wenzelm |
output more data;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 18:52:34 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2023 17:29:49 +0100 |
wenzelm |
clarified "recent" time: days <= 0 means infinity (no constraint);
|
file |
diff |
annotate
|
| Sat, 04 Nov 2023 16:56:54 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 15:38:27 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 17:17:12 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Sun, 16 Jul 2023 09:50:42 +0200 |
wenzelm |
proper close() operation;
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 11:47:43 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2023 18:32:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2023 14:22:11 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 23:25:30 +0100 |
wenzelm |
clarified signature: manage "verbose" flag via "progress";
|
file |
diff |
annotate
|
| Sun, 26 Feb 2023 20:19:01 +0100 |
wenzelm |
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2023 13:50:07 +0100 |
wenzelm |
clarified signature: more concise operations;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2023 20:40:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 22:29:24 +0100 |
wenzelm |
removed somewhat pointless support for Jenkins log files: it has stopped working long ago;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 16:08:43 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2023 15:04:15 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2022 15:52:42 +0200 |
wenzelm |
tuned signature: build_log db is specific to PostgreSQL;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2021 14:31:11 +0100 |
wenzelm |
proper fields for gnuplot (amending b614e3e4146a);
|
file |
diff |
annotate
|
| Sat, 27 Nov 2021 13:55:03 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 12 Nov 2021 23:20:05 +0100 |
wenzelm |
proper detection of ARM platform variants;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:50:00 +0100 |
wenzelm |
tuned --- avoid deprecated conversions between certain number type;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 13:04:29 +0100 |
wenzelm |
more informative errors: simplify diagnosis of spurious failures reported by users;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 22:50:09 +0100 |
wenzelm |
clarified caching;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 22:22:34 +0100 |
wenzelm |
clarified signature: absorb XZ.Cache into XML.Cache;
|
file |
diff |
annotate
|
| Sat, 28 Nov 2020 21:56:24 +0100 |
wenzelm |
added document antiquotation @{tool};
|
file |
diff |
annotate
|
| Mon, 05 Oct 2020 22:07:25 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 05 Oct 2020 21:15:58 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 26 May 2020 11:17:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Apr 2020 21:49:36 +0200 |
wenzelm |
clarified signature: more uniform treatment of stopped/interrupted state;
|
file |
diff |
annotate
|
| Sun, 13 Oct 2019 17:17:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 22:38:00 +0100 |
wenzelm |
proper data columns for plots;
|
file |
diff |
annotate
|
| Sat, 23 Feb 2019 21:48:18 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sat, 23 Feb 2019 21:33:09 +0100 |
wenzelm |
more memory fields;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2019 12:10:40 +0100 |
wenzelm |
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 15:57:24 +0100 |
wenzelm |
proper operation in weakly-typed Scala (amending 06153e2e0cdb);
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 13:53:33 +0100 |
wenzelm |
proper treatment of x86_64_32;
|
file |
diff |
annotate
|
| Sat, 19 Jan 2019 20:18:26 +0100 |
wenzelm |
more official AFP.groups;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 14:08:02 +0100 |
wenzelm |
support for user-defined Isabelle/Scala command-line tools;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2018 22:17:42 +0200 |
wenzelm |
support for XZ.Cache;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2018 21:38:27 +0100 |
wenzelm |
more compact ML_Statistics, to make build_status work with less than 2GB heap;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2018 17:37:33 +0100 |
wenzelm |
retain latest ml_stats (amending e76c6cb0d461);
|
file |
diff |
annotate
|
| Fri, 02 Mar 2018 20:46:25 +0100 |
wenzelm |
proper order;
|
file |
diff |
annotate
|
| Thu, 01 Mar 2018 20:44:38 +0100 |
wenzelm |
clarified date for presentation vs. formal pull_date;
|
file |
diff |
annotate
|
| Thu, 01 Mar 2018 20:18:24 +0100 |
wenzelm |
reveal raw data in CSV format;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2017 15:24:40 +0100 |
wenzelm |
more robust sorted_entries;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2017 14:41:26 +0100 |
wenzelm |
more convenient build_log_history;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2017 18:24:39 +0100 |
wenzelm |
proper order for entries from multiple profiles, notably "AFP";
|
file |
diff |
annotate
|
| Wed, 01 Nov 2017 17:29:14 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2017 20:26:32 +0200 |
wenzelm |
clarified output;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2017 20:14:57 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|