Re: Thoughts for 5.8.2

I believe you can push your local branch to Gitbox without issues
regardless of whether it's been pushed to GitHub before. I closed a
few GitHub pull requests by checking out from GitHub then
cherry-picking the changes from the local branch into master.

On Tue, Jun 7, 2022 at 8:45 AM Ben Weidig <[email protected]> wrote:
>
> 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]
> >
> >



-- 
Thiago