Please delete erroneously pushed branch from onionoo.git
Branch task-16907-2 should have been pushed to my public repository, but instead I pushed it to the official repository. Now I cannot delete it anymore: ``` ~/src/onionoo$ git push origin --delete task-16907-2 remote: + refs/heads/task-16907-2 onionoo karsten DENIED by fallthru remote: error: hook declined to update refs/heads/task-16907-2 To ssh://git@git-rw.torproject.org/onionoo.git ! [remote rejected] task-16907-2 (hook declined) error: failed to push some refs to 'ssh://git@git-rw.torproject.org/onionoo.git' ``` Thanks in advance!
issue