[petsc-dev] bash scripts to make PETSc development easier, less recompiles, less cut and pastes

[Jed Brown]

Barry Smith <bsmith at 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 <jed at 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