"Johannes Schindelin via GitGitGadget" <gitgitgadget@xxxxxxxxx>
writes:
> However, our GitHub workflow does not trigger on tags, therefore, this
> logic results in a missing build for that revision.
Thanks for noticing. The arrangement we had, which essentially said
"we know we will always build tagged version, so a push of a branch
that happens to have a tagged version at the tip can be ignored",
served us wonderfully. Now the maintainers of projects (not just
this one) are forbidden from tagging the tip of master, queue
something else on top and push the result out, as it won't build or
test the tagged version, which is a bit sad.
> ci/lib.sh | 2 ++
> 1 file changed, 2 insertions(+)
>
> diff --git a/ci/lib.sh b/ci/lib.sh
> index dac36886e37..f151e2f0ecb 100755
> --- a/ci/lib.sh
> +++ b/ci/lib.sh
> @@ -1,6 +1,7 @@
> # Library of functions shared by all CI scripts
>
> skip_branch_tip_with_tag () {
> + test -z "$DONT_SKIP_TAGS" || return 0
> # Sometimes, a branch is pushed at the same time the tag that points
> # at the same commit as the tip of the branch is pushed, and building
> # both at the same time is a waste.
> @@ -151,6 +152,7 @@ then
> CC="${CC:-gcc}"
>
> cache_dir="$HOME/none"
> + DONT_SKIP_TAGS=t
Quite straight-forward. Thanks, will queue.
> export GIT_PROVE_OPTS="--timer --jobs 10"
> export GIT_TEST_OPTS="--verbose-log -x"
>
> base-commit: f72f328bc57e1b0db380ef76e0c1e94a9ed0ac7c
