Re: GitHub mirror creates contribution problems

[Eduard Braun <eduard braun2 gmx de>]

Am 05.09.2017 um 16:15 schrieb Simon McVittie:
> The "default branch" on GitHub (equivalent to foo.git/HEAD in simpler
> git setups) doesn't *have* to be 'master'. My semi-official GitHub mirror of
> the reference implementation of D-Bus has its default branch set to
> 'github-placeholder', which just has a README.md; the master branch
> contains the same code as the official master branch on freedesktop.org.
Unfortunately the GitHub search only searches the default branch, though.
Personally I use GitHub mirrors of GNOME projects all the time to search 
through the code without the need to constantly check out whole repos. 
https://git.gnome.org is pretty much useless for that purpose. Your 
suggested approach makes the GitHub mirror pretty useless for that 
purpose, too (not your fault but GitHub seems reluctant to change this, 
so it might be the best one can hope for in the near future...).

Why don't you set the description of the GitHub repos accordingly 
(mention it's a mirror and where the main repo / bug tracker is)? This 
should even be possible to automate via GitHub's API: 
https://developer.github.com/v3/repos/#edit

Regards,
Eduard