Option to mirror multiple repos/users on GitHub mirror

[nikos912000]

Currently it's not possible to mirror multiple organisations or users using the GitHub mirror (correct me if I'm wrong!).

Briefly, the changes needed for this are the following:

• Define GitHubOrg in configEntry and pass it when calling the GitHub mirror. This will allow users to mirror a single organisation by passing its name to mirror-configs, which is currently not possible.
• org and user will be comma separated strings to allow multi-values.
• Additional logic here to split the strings and call getOrgRepos and getUserRepos for each org/user. The list of repos will eventually contain all repos belonging to the specified orgs and users.

I believe it's better to give flexibility to users so that they can mirror both users and orgs at the same time, i.e. this should be an if instead of an else.

@hanwen Let me know if this sounds good to you and I can raise a PR.

[hanwen]

are you sure? It seems to work just fine, see https://github.com/hanwen/zoekt-config/blob/master/mirror.json

[nikos912000]

Huh, I'd better read the docs more carefully, totally missed it. Yes, works fine when passing it in the expected format.

Out of curiosity, I see that by setting GithubUser we can mirror orgs as well? So, no need for a GithubOrg as I mentioned in my first point?

If this is the case, do we need the concept of an org and as a result its logic, i.e. getOrgRepos?

[hanwen]

I don't know, tbh. The GitHub API has separate endpoints/fields for User and Organization, but it seems they are mostly the same in practice. If you can figure out if we need to care about the difference , then that would be great.

[nikos912000]

Cool, I'll take a look once I find some time. Since this is not strictly related to the issue I'm closing it. Thanks a lot for pointing me to the right direction!