CI improvements (#1012)

2026-11-02 12:07:28 +00:00 · 2023-07-31 21:05:28 +02:00
parent 0b95ef09b7
commit b14c741422
7 changed files with 70 additions and 6 deletions
@@ -5,6 +5,7 @@ on: [pull_request, merge_group]
 jobs:
  build:
    runs-on: ubuntu-latest
+    # Don't run in the merge queue again if the branch is up to date with `develop`
    if: github.event.merge_group.base_ref != 'refs/heads/develop'
    name: Validate
    steps: