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