Closes #15 (closed).
enabled an automatic merge when the pipeline for 82653d2f succeeds
merged
mentioned in commit 4a660df5
Thx for reporting. Supposedly fixed by this.
