| Thu, 26 Nov 2020 17:23:33 +0100 | wenzelm | clarified options: batch-build has pide_reports disabled by default (requires significant resources); | changeset | files |
| Thu, 26 Nov 2020 17:01:19 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 26 Nov 2020 16:51:40 +0100 | wenzelm | proper return code for more errors (amending d892f6d66402); | changeset | files |