Wed, 16 Aug 2023 14:42:43 +0200 | wenzelm | build_worker is stopped independently from master build_process; | file | diff | annotate |
Thu, 10 Aug 2023 16:57:01 +0200 | wenzelm | more robust; | file | diff | annotate |
Thu, 10 Aug 2023 16:49:17 +0200 | wenzelm | tuned signature; | file | diff | annotate |