workflows/{pr,push}: init

Those two workflows bundle all the main jobs in two event-specific
wrapper workflows. This enables us to do two things later on:
- Synchronize the merge commits between most of the jobs run in a PR.
- Create a single "required" job to be targeted by GitHub's "required
status checks to pass" feature.

(cherry picked from commit 959eed1f2a)
This commit is contained in:
Wolfgang Walther
2025-06-08 12:12:06 +02:00
committed by github-actions[bot]
parent 6685212040
commit 9eb06853d9
9 changed files with 96 additions and 48 deletions

View File

@@ -1,14 +1,7 @@
name: Check
on:
pull_request:
paths:
- .github/workflows/check.yml
pull_request_target:
concurrency:
group: check-${{ github.workflow }}-${{ github.event_name }}-${{ github.event.pull_request.number || github.run_id }}
cancel-in-progress: true
workflow_call:
permissions: {}