This resolves #820 (closed).
enabled an automatic merge when the pipeline for a43db543 succeeds
merged
mentioned in commit f5f4d2b9