Barry Smith <bsm...@petsc.dev> writes: > Nice, I didn't know about that alternative, I'll check it out.
AFAIK, there is still no push option to run a pipeline. There's an option ci.skip if you're configured to run by default. If developers set ci.skip as a default push option, we could re-enable the default case. >> On Jun 18, 2020, at 9:21 PM, Jed Brown <j...@jedbrown.org> wrote: >> >> Cool! Note that you can do things like this without going through the API >> >> git push -o merge_request.create -o merge_request.target=maint
