I am curious what would happen if you merge in github, then pull, then
push to code? Would "the right thing" happen?
-derek
Christian Stimming writes:
> Am Freitag, 3. Januar 2020, 23:19:13 CET schrieb John Ralls:
>> Christian,
>>
>> Well, it does disable the merge button. "applies to adminis
I think so, as long as you pull before anyone pushes something to code and that
blows away your merge. Of course if someone then pushes to code before you get
the merge pushed you'll have a bit of cleanup work before you're able to push.
Regards,
John Ralls
> On Jan 8, 2020, at 12:26 PM, Derek
