Help unsticking the git -> GitHub mirroring

[Till Westmann]

Hi,

it seems it’s stuck again. I’ve did a mini fix to unblock it:

https://asterix-gerrit.ics.uci.edu/710

Whoever reads this first, please review :)

Thanks,
Till