gcc-wwwdocs branch python-formatting created. e1e17c97a8ae35cfb6b2f7428fb52b05f82450d1

[Mark Wielaard]

Hi Gerald,

On Mon, Dec 02, 2024 at 12:13:35AM +0100, Gerald Pfeifer wrote:
> 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:
> > 
> > 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

Yes, everything looks fine now, the (remote) branch is gone.

Thanks,

Mark