Commit 3096f6e8 authored by Lorenz Huedepohl's avatar Lorenz Huedepohl

Merge branch 'master' into 'master'

Fix CI

It was more involved than I initially thought! But seems to be working now.

See merge request !3
parents ec1e3dc0 c1986aaf
Pipeline #69886 passed with stage
in 44 seconds