Follow-up Comment #1, sr #106896 (project administration):
I've found out how to delete remote branches:
git push ${log...@git.sv.gnu.org:/srv/git/${project}.git
:heads/${branch2delete}
deleting the remote *master* however seems to have screwed up the
repository.
warning: remote HEAD refers to nonexistent ref, unable to checkout.
_______________________________________________________
Reply to this item at:
<http://savannah.gnu.org/support/?106896>
_______________________________________________
Message sent via/by Savannah
http://savannah.gnu.org/
