Re: new procedure with GitLab CI

[David Kastrup]

Jonas Hahnfeld <address@hidden> writes:

> Am Sonntag, den 24.05.2020, 13:19 +0100 schrieb James Lowe:
>
>> So, and you didn't answer this specific question, if I set the label to 
>> 'review' before the pipeline runs will make doc still run?
>
> Sorry: Yes, CI pipelines will run irrespective of the labels.

One note for submissions: one can do a push using

git push -o ci.skip

and as far as I understand, no CI will happen.  "skip" does sound like
no CI would even be required for letting the patch move on, so it will
likely depend on the discretion of the submitter to not follow up with
an actual merge.

-- 
David Kastrup