Re: Thoughts for 5.8.2

Hi Volker,

I've switched to GitBox because it's the canonical remote and not just the
mirrored one.
It seems that Apache had some infrastructure issues lately affecting the
mirroring, which caused the remotes to differ.
My train of thought is that I don't want to merge back a branch to master
that isn't even present on GitBox, because I'm not sure how GitBox would
react.

But maybe the easiest way forward is creating a diff, deleting the branch
on GitHub, and committing/pushing the diff on GitBox.


On Tue, Jun 7, 2022 at 1:38 PM Volker Lamp <[email protected]> wrote:

> Hi Ben
>
> > Any suggestions for the best way to solve this?
> > So far, I've worked with GitHub, but now I've switched my repo's remote
> > origin to GitBox.
> > Should I just push the branch to GitBox and hope for the best that
> > mirroring works and nothing clashes with the pre-existing branch?
> > Delete the GitHub branch first?
>
> How about setting origin back to GitHub? That way you'd at least push to a
> repo that already has the branch.
>
> ---------------------------------------------------------------------
> To unsubscribe, e-mail: [email protected]
> For additional commands, e-mail: [email protected]
>
>