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

Jed Brown jed at jedbrown.org
Thu Jun 18 21:33:01 CDT 2020

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

>> 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

More information about the petsc-dev mailing list