Commit 69db45a5 authored Jan 25, 2024 by Jan Kiene

Merge branch 'ci/change-instrumented-build-job-to-avoid-problems-on-certain-runners' into 'main'

[CI] change instrumented build job to avoid problems on certain runners

See merge request !1340