-
Simon McVittie authored
When we push to master it's usually for one of three reasons: 1. We merged a merge request 2. We pushed the "release vX.Y.Z" commit, together with a tag 3. We pushed some other trivial change directly When we merged a merge request, immediately running CI is not necessarily very helpful, because we already ran it for the branch that's getting merged. If we pushed a release commit and a tag, we want the CI pipeline for the tag to take priority over the CI pipeline for the release commit. If we pushed a trivial change, it might not even need CI (if it's just a change to a README, or similar), but if it does, we can trigger it manually. Signed-off-by:
Simon McVittie <smcv@collabora.com>
Simon McVittie authoredWhen we push to master it's usually for one of three reasons: 1. We merged a merge request 2. We pushed the "release vX.Y.Z" commit, together with a tag 3. We pushed some other trivial change directly When we merged a merge request, immediately running CI is not necessarily very helpful, because we already ran it for the branch that's getting merged. If we pushed a release commit and a tag, we want the CI pipeline for the tag to take priority over the CI pipeline for the release commit. If we pushed a trivial change, it might not even need CI (if it's just a change to a README, or similar), but if it does, we can trigger it manually. Signed-off-by:
Simon McVittie <smcv@collabora.com>