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
! [remote rejected] dicts-strict (hook declined)
Git gurus chime in? Thanks.