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 <vl...@apache.org> 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: dev-unsubscr...@tapestry.apache.org > For additional commands, e-mail: dev-h...@tapestry.apache.org > >
