Merge pull request 'ci: drop push:dev trigger; PR is the gate' (#25) from dev into main
This commit was merged in pull request #25.
This commit is contained in:
@@ -4,8 +4,10 @@ name: test
|
|||||||
# locally via docker-compose; they should guard with testing.Short().
|
# locally via docker-compose; they should guard with testing.Short().
|
||||||
|
|
||||||
on:
|
on:
|
||||||
push:
|
# PRs against main are the gate. Direct pushes to dev no longer trigger
|
||||||
branches: [dev]
|
# CI on their own — opening a PR fires the pull_request event and gates
|
||||||
|
# the merge. Avoids the duplicate push+pull_request runs we were
|
||||||
|
# accumulating on every PR commit.
|
||||||
pull_request:
|
pull_request:
|
||||||
branches: [main]
|
branches: [main]
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user