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

[Max Bolingbroke]

On 28 June 2011 08:23, Max Bolingbroke <batterseapower at hotmail.com> wrote:
> On 28 June 2011 07:52, Max Bolingbroke <batterseapower at hotmail.com> wrote:
>> On 25 June 2011 19:19, Johan Tibell <johan.tibell at gmail.com> wrote:
>>> Perhaps not. Just asking if they intend to support --mirror would be useful.
>>
>> I've used the contact form on their website to ask. Let's see what they say.
>
> Apparently they do intend to support it and this is indeed a bug.
> Furthermore, they have offered to set up automatic mirroring on their
> end, which will work around the problem (and make our lives easier, as
> in theory we won't have to maintain it). I've sent them a list of the
> upstream URLs corresponding to each of the mirrored repositories on
> GitHub.

Tekkub from GitHub has just got back to me telling me that the mirrors
have been set up.

(It took a while because he wanted to write a script to set up the
mirrors, since we had ~19 repositories to mirror). He says "It may
take a little time for them all to sync."

In theory we can now remove the push --mirror lines from our scripts
(though for some reason they have stopped giving me an error). I'm
going to do this now.

Max