Nicolas c4ef989e1a ci: drop pull_request trigger, push alone covers same-repo PRs ... push (all branches) already fires for a PR branch on this repo; keeping pull_request too just ran every job twice on the same commit. GitHub still attaches the push-triggered run to the PR by SHA regardless of which event fired it. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>		2026-08-17 23:14:46 +02:00
..
workflows	ci: drop pull_request trigger, push alone covers same-repo PRs	2026-08-17 23:14:46 +02:00