Follow-up Comment #1, sr #107353 (project administration): just do a delete-push to delete the remote branch and then push the new branch.
The server-side check is of some value but can rightfully be worked around
when needed (as you do).
_______________________________________________________
Reply to this item at:
<http://savannah.gnu.org/support/?107353>
_______________________________________________
Message sent via/by Savannah
http://savannah.gnu.org/
