Re: new procedure with GitLab CI

[Valentin Villenave]

On 5/27/20, Jonas Hahnfeld <address@hidden> wrote:
> Pinging this to attention...

Yeah, that’s one of those “I’ve read it without fully understanding
it” situations (and then the discussion devolved into James’s workflow
and I lost track).

So IIUC there’s no way to skip the rebase-triggered CI pipeline right
now?  (I didn’t quite understand if the -skip option worked or not in
that case.)
Or are we willing to accept situations where, in case of a fairly
trivial rebase where side-effects are absolutely unlikely, people
could manually stop the pipeline as soon as it starts, and force the
merge to happen immediately?

Cheers,
-- V.