Manuel M T Chakravarty writes:
I think, it also only mirrors master, but not other branches, which is unfortunate especially for release branches.
Fixed on both counts. The GitHub mirror should be both up-to-date and
include all branches.
Cheers,
- Ben
