Guessing process:
Maintainer picked and applied PR commit, and pushed to git.openwrt.org
Maintainer force-pushed (upstream) commit to PR fork branch, for github bot to mark merged PR.
This triggered CI runs for PR / fork:
Ideally we detect when a CI run has triggered on an identical git tree state to avoid this.
Choices around what we do here (cancel the PR run?), given different branches can have different actions.
Situation was: Pull request (PR) open, ready to merge https://github.com/openwrt/openwrt/pull/13021
Guessing process: Maintainer picked and applied PR commit, and pushed to git.openwrt.org Maintainer force-pushed (upstream) commit to PR fork branch, for github bot to mark merged PR. This triggered CI runs for PR / fork:
Github OpenWrt mirror has picked up the git.openwrt.org changes, and started duplicate CI runs:
Both these sets of CI actions ran on https://github.com/openwrt/openwrt/commit/b3448b3fdb59d25dce05991dc8f322c1020b090b, the first via the PR / fork. Duplicate usage time was over six hours.
Ideally we detect when a CI run has triggered on an identical git tree state to avoid this. Choices around what we do here (cancel the PR run?), given different branches can have different actions.
Cheers