Delete a branch from trac

[Chaman Agrawal]

Hi folks,

While pushing my code, by mistake I have made a new branch in trac (public/ticket/24894_superRSK) using the command `git push trac HEAD:public/ticket/24894_superRSK` instead of using my old branch. Now I want to delete this branch since it's not required but how to do so?

Thanks,

Chaman Agrawal

[Frédéric Chapoton]

git push trac :public/ticket/24894_superRSK