CI: update filters
Update the filters to make the CI happy again. This was not caught by the CI actions of #3027, as the PR had been open for too long.
Please register or sign in to comment
Update the filters to make the CI happy again. This was not caught by the CI actions of #3027, as the PR had been open for too long.