| Wed, 06 Aug 2025 16:51:58 +0200 | Fabian Huch | tuned doc: display build manager SSH options; | file | diff | annotate | 
| Wed, 09 Apr 2025 22:23:59 +0200 | wenzelm | tuned: prefer explicit Bash.exports; | file | diff | annotate | 
| Thu, 27 Mar 2025 10:45:33 +0100 | Fabian Huch | start jobs even if repository is unreachable, e.g. due to high load; | file | diff | annotate | 
| Sun, 02 Feb 2025 00:11:06 +0100 | Fabian Huch | clarified name; | file | diff | annotate | 
| Sat, 01 Feb 2025 22:41:43 +0100 | Fabian Huch | tuned; | file | diff | annotate | 
| Sat, 01 Feb 2025 22:39:44 +0100 | Fabian Huch | use ssh host for default address; | file | diff | annotate | 
| Sat, 01 Feb 2025 22:30:09 +0100 | Fabian Huch | clarified option name; | file | diff | annotate | 
| Sat, 01 Feb 2025 22:28:32 +0100 | Fabian Huch | clarified options: extra ssh connection to cluster of build_manager; | file | diff | annotate | 
| Sat, 01 Feb 2025 22:20:42 +0100 | Fabian Huch | tuned output; | file | diff | annotate | 
| Sat, 01 Feb 2025 20:46:01 +0100 | Fabian Huch | tuned: more standard; | file | diff | annotate | 
| Mon, 20 Jan 2025 09:17:37 +0100 | Fabian Huch | clarified; | file | diff | annotate | 
| Fri, 17 Jan 2025 13:43:16 +0100 | Fabian Huch | tuned whitespace; | file | diff | annotate | 
| Tue, 27 Aug 2024 13:53:18 +0200 | Fabian Huch | stop web server on close; | file | diff | annotate | 
| Tue, 27 Aug 2024 13:44:23 +0200 | Fabian Huch | better results for terminated jobs; | file | diff | annotate | 
| Tue, 27 Aug 2024 13:12:10 +0200 | Fabian Huch | more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated; | file | diff | annotate | 
| Tue, 27 Aug 2024 12:57:49 +0200 | Fabian Huch | manage runner state properly (amending be4c1fbccfe8); | file | diff | annotate | 
| Wed, 21 Aug 2024 13:33:19 +0200 | Fabian Huch | remove terminated jobs, even if futures do not complete; | file | diff | annotate | 
| Tue, 20 Aug 2024 17:28:51 +0200 | Fabian Huch | terminate jobs properly; | file | diff | annotate | 
| Tue, 06 Aug 2024 18:39:32 +0200 | Fabian Huch | build_manager: change colors; | file | diff | annotate | 
| Tue, 06 Aug 2024 16:58:23 +0200 | Fabian Huch | build_manager: display more info; | file | diff | annotate | 
| 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 |