On Fri, 23 Aug 2024, Eric Gallager wrote: >>> The branch, python-formatting has been created >>> at e1e17c97a8ae35cfb6b2f7428fb52b05f82450d1 (commit) >> Hmm, are you intentionally creating a branch for the wwwdocs repository >> (i.e., our web pages)? I don't recall us having used one before. > Sorry about that, I'd meant to create it just for my copy of the repo > that's mirrored to GitHub, but pushed it to the wrong remote by > accident.
I tried to delete it via # git push origin --delete remotes/origin/python-formatting alas just get error: unable to delete 'remotes/origin/python-formatting': remote ref does not exist Any idea how to drop that branch again from the main gcc.gnu.org repo? Gerald
