| Tue, 06 Aug 2024 15:40:51 +0200 | Fabian Huch | tuned and clarified; | file | diff | annotate |
| Tue, 06 Aug 2024 15:38:10 +0200 | Fabian Huch | build_manager: store submitting user; | file | diff | annotate |
| Tue, 06 Aug 2024 15:00:37 +0200 | Fabian Huch | build_manager: terminate processes if cancelling does not work; | file | diff | annotate |
| Tue, 06 Aug 2024 13:54:10 +0200 | Fabian Huch | build_manager: log message when job is cancelled; | file | diff | annotate |
| Thu, 18 Jul 2024 13:52:51 +0200 | Fabian Huch | better poller: don't start job when same version is already running; | file | diff | annotate |
| Thu, 18 Jul 2024 13:08:11 +0200 | Fabian Huch | clarified: more uniform; | file | diff | annotate |
| Wed, 10 Jul 2024 17:42:48 +0200 | Fabian Huch | tuned website; | file | diff | annotate |
| Wed, 10 Jul 2024 17:31:17 +0200 | Fabian Huch | proper parse (amending dd86d35375a7); | file | diff | annotate |
| Wed, 10 Jul 2024 17:04:44 +0200 | Fabian Huch | allow updating reports via build_manager_database tool, e.g. to generate hg logs/diffs; | file | diff | annotate |
| Wed, 10 Jul 2024 17:01:51 +0200 | Fabian Huch | clarified; | file | diff | annotate |
| Wed, 10 Jul 2024 16:58:39 +0200 | Fabian Huch | clarified; | file | diff | annotate |
| Wed, 10 Jul 2024 16:56:59 +0200 | Fabian Huch | log and display components with empty (unknown) revisions to indicate that they are present; | file | diff | annotate |
| Wed, 10 Jul 2024 09:58:32 +0200 | Fabian Huch | tuned log: omit previous changeset; | file | diff | annotate |
| Tue, 09 Jul 2024 16:06:32 +0200 | Fabian Huch | tuned display; | file | diff | annotate |
| Tue, 09 Jul 2024 15:06:24 +0200 | Fabian Huch | tuned HTML display of ANSI colors for better readability; | file | diff | annotate |
| Tue, 09 Jul 2024 14:13:59 +0200 | Fabian Huch | render hg diff and log (on separate page); | file | diff | annotate |
| Tue, 09 Jul 2024 13:58:43 +0200 | Fabian Huch | clarified; | file | diff | annotate |
| Tue, 09 Jul 2024 12:56:27 +0200 | Fabian Huch | store hg log in addition to diff; | file | diff | annotate |
| Tue, 09 Jul 2024 11:20:09 +0200 | Fabian Huch | clarified names; | file | diff | annotate |
| Tue, 09 Jul 2024 11:11:15 +0200 | Fabian Huch | tuned; | file | diff | annotate |
| Sat, 06 Jul 2024 11:18:31 +0200 | wenzelm | tuned messages: whitespace following usual Isabelle conventions; | file | diff | annotate |
| Fri, 05 Jul 2024 10:38:17 +0200 | Fabian Huch | tuned whitespace; | file | diff | annotate |
| Fri, 05 Jul 2024 09:52:56 +0200 | Fabian Huch | use ansi colored diffs; | file | diff | annotate |
| Fri, 05 Jul 2024 09:47:21 +0200 | Fabian Huch | add diffs to build manager; | file | diff | annotate |
| Thu, 04 Jul 2024 13:50:14 +0200 | Fabian Huch | clarified: components vs. extra components; | file | diff | annotate |
| Thu, 04 Jul 2024 09:57:40 +0200 | Fabian Huch | compress reports; | file | diff | annotate |
| Wed, 03 Jul 2024 21:11:24 +0200 | Fabian Huch | clarified build report; | file | diff | annotate |
| Mon, 01 Jul 2024 15:25:27 +0200 | Fabian Huch | tuned; | file | diff | annotate |
| Mon, 01 Jul 2024 15:24:04 +0200 | Fabian Huch | add timeout to build manager tasks/jobs (e.g. for cluster builds that don't terminate after error on host); | file | diff | annotate |
| Mon, 01 Jul 2024 14:46:51 +0200 | Fabian Huch | clarified: more operations; | file | diff | annotate |
| Mon, 01 Jul 2024 14:31:30 +0200 | Fabian Huch | tuned website; | file | diff | annotate |
| Fri, 28 Jun 2024 17:13:25 +0200 | Fabian Huch | abort tasks with invalid host specs; | file | diff | annotate |
| Fri, 28 Jun 2024 16:18:40 +0200 | Fabian Huch | tuned cli; | file | diff | annotate |
| Fri, 28 Jun 2024 13:49:29 +0200 | Fabian Huch | proper build command; | file | diff | annotate |
| Fri, 28 Jun 2024 12:10:26 +0200 | Fabian Huch | tuned website; | file | diff | annotate |
| Fri, 28 Jun 2024 11:51:46 +0200 | Fabian Huch | better results view; | file | diff | annotate |
| Fri, 28 Jun 2024 11:33:09 +0200 | Fabian Huch | better build summaries; | file | diff | annotate |
| Fri, 28 Jun 2024 09:54:06 +0200 | Fabian Huch | clarified: more operations; | file | diff | annotate |
| Thu, 27 Jun 2024 09:41:16 +0200 | Fabian Huch | add Isabelle settings to managed tasks and ci jobs; | file | diff | annotate |
| Wed, 12 Jun 2024 17:12:13 +0200 | Fabian Huch | moved ci_build module to build_ci; | file | diff | annotate |
| Wed, 12 Jun 2024 17:06:34 +0200 | Fabian Huch | overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions; | file | diff | annotate |
| Tue, 25 Jun 2024 18:09:53 +0200 | Fabian Huch | tuned; | file | diff | annotate |
| Tue, 25 Jun 2024 17:57:08 +0200 | Fabian Huch | tuned; | file | diff | annotate |
| Tue, 25 Jun 2024 17:56:49 +0200 | Fabian Huch | add root entry for non-local components; | file | diff | annotate |
| Tue, 25 Jun 2024 17:55:37 +0200 | Fabian Huch | clarified; | file | diff | annotate |
| Tue, 25 Jun 2024 13:53:45 +0200 | Fabian Huch | extra timer delay, to limit db transactions; | file | diff | annotate |
| Tue, 25 Jun 2024 13:44:20 +0200 | Fabian Huch | proper synchronized; | file | diff | annotate |
| Sun, 16 Jun 2024 21:54:09 +0200 | wenzelm | merged | file | diff | annotate |
| Sun, 16 Jun 2024 18:41:57 +0200 | wenzelm | Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String); | file | diff | annotate |
| Wed, 12 Jun 2024 10:47:53 +0200 | Fabian Huch | tuned messages; | file | diff | annotate |
| Wed, 12 Jun 2024 08:52:36 +0200 | Fabian Huch | clarified web server paths; | file | diff | annotate |
| Tue, 11 Jun 2024 11:07:48 +0200 | Fabian Huch | proper available hosts; | file | diff | annotate |
| Tue, 11 Jun 2024 10:30:55 +0200 | Fabian Huch | tuned comments; | file | diff | annotate |
| Tue, 11 Jun 2024 08:58:22 +0200 | Fabian Huch | add build_manager_database tool to restore db from log files; | file | diff | annotate |
| Mon, 10 Jun 2024 18:45:21 +0200 | Fabian Huch | use build log in build manager to store meta-data persistently; | file | diff | annotate |
| Mon, 10 Jun 2024 17:08:47 +0200 | Fabian Huch | improve build manager log (for build_log); | file | diff | annotate |
| Mon, 10 Jun 2024 16:37:16 +0200 | Fabian Huch | clarified; | file | diff | annotate |
| Mon, 10 Jun 2024 16:14:44 +0200 | Fabian Huch | proper web server address; | file | diff | annotate |
| Mon, 10 Jun 2024 16:02:53 +0200 | Fabian Huch | clarified names: more canonical; | file | diff | annotate |
| Mon, 10 Jun 2024 15:13:21 +0200 | Fabian Huch | clarified; | file | diff | annotate |