delete remote branch

Herbert Valerio Riedel hvr at
Sun Sep 8 08:43:21 UTC 2013

Hello Nicolas,

On 2013-09-08 at 09:41:04 +0200, Nicolas Frisby wrote:
> I just merged in my -fdicts-strict work, so I was deleting the old branch…
> but it's rejected for some reason.
> $ git push origin --delete dicts-strict
> remote: performing tab-check...
> remote: + refs/heads/dicts-strict ghc <my-username> DENIED by fallthru
> remote: error: hook declined to update refs/heads/dicts-strict
> To ssh://
>  ! [remote rejected] dicts-strict (hook declined)
> error: failed to push some refs to 'ssh://'
> Git gurus chime in? Thanks.

The current configuration doesn't permit risky operations, such as
deleting branches and/or non-forward-updates (imagine someone would
delete or rebase branches such as 'master' or 'ghc-7.6'). Moreover,
having commits disappear causes headaches with other facilities
(e.g. git submodules).

Moreover, it was planned to define a Git ref namespace, where those
operations would be allowed to everybody, something like 'wip/*' (see
[1] for an example). Those branches could then also be made to be
ignored by the Git email notifier, so that rebasing commits doesn't spam
the Git commits mailing list.

In the long-term, we should avoid cluttering the top-level branch
namespace[2] with topic branches, and move to a more structured naming
scheme, which leaves the top-level namespace to release branches.

Long story short, I've deleted the 'dicts-strict' branch for you



More information about the ghc-devs mailing list