Verified Commit dd8830cc authored by georg's avatar georg

CI: deploy: ignore 'dev' directory (regression fix)

Otherwise, if the master branch is deployed, the 'dev' directory is
removed, which possibly contains data we want to keep, for example code
coverage reports or proposed website changes.

This commit fixes a regression introduced in

It was tested via an intermediate commit to ensure it works as expected.

Relates !71
parent e7827555
Pipeline #24196 passed with stages
in 37 seconds