fixes #858 (closed)
enabled an automatic merge when the pipeline for 5f41ee88 succeeds
mentioned in commit f288178b
merged