| 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 |
| Mon, 10 Jun 2024 14:08:15 +0200 | Fabian Huch | remove unused; | file | diff | annotate |
| Mon, 10 Jun 2024 14:03:19 +0200 | Fabian Huch | tuned; | file | diff | annotate |
| Mon, 10 Jun 2024 13:55:59 +0200 | Fabian Huch | add title; | file | diff | annotate |
| Mon, 10 Jun 2024 13:45:12 +0200 | Fabian Huch | use build_cluster in ci builds; | file | diff | annotate |
| Fri, 07 Jun 2024 19:14:36 +0200 | Fabian Huch | add favicon to web app; | file | diff | annotate |
| Fri, 07 Jun 2024 18:50:46 +0200 | Fabian Huch | build manager: echo error messages to server output; | file | diff | annotate |
| Fri, 07 Jun 2024 18:16:50 +0200 | Fabian Huch | omit showing previous failures for user builds; | file | diff | annotate |
| Fri, 07 Jun 2024 17:40:12 +0200 | Fabian Huch | always handle interrupted jobs; | file | diff | annotate |
| Fri, 07 Jun 2024 15:47:19 +0200 | Fabian Huch | add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware; | file | diff | annotate |
| Fri, 07 Jun 2024 15:04:07 +0200 | Fabian Huch | clarified context: operations now in build process; | file | diff | annotate |
| Fri, 07 Jun 2024 14:00:59 +0200 | Fabian Huch | clarified: add explicit build process; | file | diff | annotate |
| Fri, 07 Jun 2024 13:54:00 +0200 | Fabian Huch | remove unnecessary subdir; | file | diff | annotate |
| Fri, 07 Jun 2024 13:52:25 +0200 | Fabian Huch | tuned; | file | diff | annotate |
| Thu, 06 Jun 2024 22:26:40 +0200 | wenzelm | clarified names; | file | diff | annotate |
| Thu, 06 Jun 2024 22:13:10 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Thu, 06 Jun 2024 22:03:20 +0200 | wenzelm | tuned whitespace; | file | diff | annotate |
| Thu, 06 Jun 2024 21:48:36 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Thu, 06 Jun 2024 14:51:28 +0200 | Fabian Huch | add triggers to ci jobs: on commit vs timed; | file | diff | annotate |
| Thu, 06 Jun 2024 13:37:27 +0200 | Fabian Huch | manage components of ci builds; | file | diff | annotate |
| Thu, 06 Jun 2024 09:04:01 +0200 | Fabian Huch | use external CSS for build manager page; | file | diff | annotate |
| Thu, 06 Jun 2024 08:58:58 +0200 | Fabian Huch | more build manager page; | file | diff | annotate |
| Wed, 05 Jun 2024 17:41:16 +0200 | Fabian Huch | ensure permissions when starting build task (e.g., due to misconfigured client); | file | diff | annotate |
| Wed, 05 Jun 2024 17:27:13 +0200 | Fabian Huch | add verbose option to build_task; | file | diff | annotate |
| Wed, 05 Jun 2024 15:01:20 +0200 | Fabian Huch | build manager: manage directories/permissions, to minimize local administration; | file | diff | annotate |
| Tue, 04 Jun 2024 18:55:55 +0200 | Fabian Huch | read prefs properly; | file | diff | annotate |
| Tue, 04 Jun 2024 18:43:04 +0200 | Fabian Huch | allow explicit Isabelle rev in build task (e.g., for older Isabelle versions); | file | diff | annotate |
| Tue, 04 Jun 2024 09:02:36 +0200 | Fabian Huch | add build manager module; | file | diff | annotate |