On Sun, 1 Dec 2024, Gerald Pfeifer wrote:
> 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? You have to use the name of the branch in the remote repo, "python-formatting": git push --delete origin python-formatting (or using the colon syntax:) git push origin :python-formatting Alexander
