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
|
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
|