gcc-wwwdocs branch python-formatting created. e1e17c97a8ae35cfb6b2f7428fb52b05f82450d1

[Gerald Pfeifer]

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