On Sun, 1 Dec 2024, Alexander Monakov wrote:
> You have to use the name of the branch in the remote repo,
> "python-formatting":
>
> git push --delete origin python-formatting
That did the job, thank you!
On Sun, 1 Dec 2024, Mark Wielaard wrote:
> I believe the correct invocation is:
>
> $ git push origin --delete python-formatting
>
> against your local repo where your origin is
> ssh://ger...@gcc.gnu.org/git/gcc-wwwdocs.git
>
> If that doesn't work we'll have to clean it up on the server.
I believe things are fine?
% git branch -la | cat
* master
remotes/origin/HEAD -> origin/master
remotes/origin/master
Thanks,
Gerald
