The push trigger was already restricted to master and to source paths,
but pull_request carried only a branch filter — so a PR touching nothing
but the README would have run a full build. A branch filter constrains
where a workflow fires, not what fires it.
Both filters now list the same six paths. A docs-only change runs nothing,
on either trigger.
Note that .github/workflows/** is deliberately absent from both lists, so
editing this file does not run it. That is the intended trade: fewer
pointless builds, at the cost of a broken workflow surfacing on the next
source change rather than immediately.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WHt4DykxXaQnyaJfyS8KCn
mikkeli
7a92485cf1