This resolves #818 (closed).
Pipeline #118789 passed
Pipeline passed for 1d6bcf04 on j.det3 1 year ago
Pipeline #118816 passed
Pipeline passed for cd171f76 on main 1 year ago
enabled an automatic merge when the pipeline for 1d6bcf04 succeeds
merged
mentioned in commit cd171f76