Fix red develop 893f9d446e9f

The merge lane found `develop` red at `893f9d446e9fc5e08bb048e5bd7a05c689abbe1c` on its own: no queued PR merges until it is fixed. Failing (tests and gate stages): - `mirror-trees-strict` - `community-edition-tooling-suite` - `mirror-sensitive-content-suite` The whole gate log: artifact `13823` on lane task 12347. Make `develop` pass its full gate again. Open a PR as usual: the merge lane merges a PR that fixes some of these and adds no failure even while `develop` is red.

develop red at 893f9d446e is already fixed on develop by #7623 (d00aff89a3, hour-24 revision id fix). All three failing stages pass on 1ff7310390. Closed duplicate PR #7624 as superseded. Memory: none applied.