Simon Peyton Jones via ghc-devs writes:
I'm getting lots of the messages below.
Running 'git prune' makes no difference.
Simon
Indeed, the warning is on the server side (hence the "remote:" prefix).
I'll need to take care of this on the server.
Cheers,
- Ben
