Re: new procedure with GitLab CI

[David Kastrup]

Jonas Hahnfeld <address@hidden> writes:

> Am Sonntag, den 24.05.2020, 16:28 +0200 schrieb 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.
>
> You can also put "[skip ci]" in the commit message. However I think
> this only applies to pipelines on commits. Pipelines for merge requests
> could maybe still run, I haven't tested this.
> Eventually GitLab requires that there is a passing pipeline before a
> merge. If you cancel the pipeline, I verified GitLab is not fooled. I
> hope it's the same for skips, but again haven't tested.
>
> If you remember, could you try it with one of your next MRs?

<https://gitlab.com/lilypond/lilypond/-/merge_requests/88>

I don't see that my use of -o ci.skip had any effect so far: the
pipeline appears to be running.

-- 
David Kastrup