Github push hook failure: "can't push to the refs/pull/* hierarchy"

[Max Bolingbroke]

On 24 June 2011 16:09, Johan Tibell <johan.tibell at gmail.com> wrote:
> Are you sure this is the case? If so we should perhaps file a bug on
> GitHub to get that working.
>
> I thought --mirror essentially did a -f.

Yes it does, but that's not the problem. The problem is that --mirror
deletes refs from the remote (i.e. GitHub) that are not present
locally. And GitHub creates some special remotes to track pull
requests, and does not want them to be deleted!

I'm not sure if that can really be counted as a GitHub bug. Do you
think it's worth asking?

Max