On 14/09/2023 01:30, Jeff King wrote:
On Wed, Sep 13, 2023 at 04:16:48PM +0100, Phillip Wood wrote:
We can do the loop-unroll thing if we really want to support multiple
prefixes, but if you're OK with it, let's try the single-prefix way and
see if anybody runs into problems (I'm still convinced there's only a
few of us using this stuff anyway). I'm hesitant to do the unroll just
because it requires picking a maximum value, with a bizarre failure if
you happen to have 4 prefixes or whatever.
Lets start with a single-prefix and see if anyone complains
Aside: what I'd really like is to be able to set an environment variable
when I push to skip or force the CI
GITHUB_SKIP_CI=1 git push github ...
but that would require support from the git client, the protocol and the
server.
We have the necessary bits at the protocol: push-options. But it's up to
the server-side hooks to decide which ones are meaningful and to do
something useful with them. It looks like GitLab supports:
git push -o ci.skip=1 ...
Oh I didn't know about that
but I don't think GitHub respects any equivalent option.
That's a shame
Best Wishes
Phillip
