Fix coverage-report deploy
Deploy of coverage reports to gitlab pages accidentally got broken in !398 (merged).
Edited by Frederik Hennig
Deploy of coverage reports to gitlab pages accidentally got broken in !398 (merged).
added Bug label
requested review from @holzer
assigned to @da15siwa
changed the description
approved this merge request
enabled an automatic merge when the pipeline for 8dcf013d succeeds
merged
mentioned in commit 8658a203