Hey,
sorry, I'm a little late to respond. I didn't push to GitHub, at least not consciously.
Let me know if you find that I screwed up somewhere.
Cheers,
Sebastian
________________________________
Von: Ben Gamari
Almost every day now I receive an e-mail from GitLab titled "Remote mirror update failed", which contains something like:
To
! [remote rejected] wip/dmd-arity -> wip/dmd-arity (cannot lock ref 'refs/heads/wip/dmd-arity': is at e1cc1254b81a7adadd8db77c7be625497264ab2b but expected f07b61d047967129a3ae0c56f8894d41c5a9b036)
error: failed to push some refs to '[FILTERED]@github.com/ghc/ghc'
Hmm, how annoying. Strangely, the `wip/dmd-arity` branch currently appears to be sitting at the same commit on GitLab and GitHub so I'm not really sure what to do here. sgraf, did you ever push a branch manually to the github.com/ghc/ghc mirror? Cheers, - Ben