CI: merge linting jobs into one
Passed
Reiter, Christoph
created pipeline for commit
f3875064
, finished
For main
1 minute 13 seconds, queued for 7 seconds