> > I can confirm I was able to delete a branch on remove server: > > > > $ git push origin --delete refs/users/marxin/heads/gfc-trailing-spec > > To git+ssh://gcc.gnu.org/git/gcc.git > > - [deleted] refs/users/marxin/heads/gfc-trailing-spec > > That's because I fixed GCC's hook to allow branch deletion: > https://gcc.gnu.org/pipermail/gcc/2020-October/233914.html
Interesting that you would manage this aspect yourselves. The git-hooks have a config option that allow to control which branch can be deleted (via a list of regular expressions). -- Joel