Github mirrors

We are mirroring our [major] git repositories on github, specifically in the osmocom github organization

Old-style mirrors (github server-based)

Until October 2017, all mirrors are server-based mirrors at github, where github once per hour polls our repository and mirrors it over.

This configuration is not possible to do as a github user, but it requires manual configuration by github staff.

New-style mirrors (gerrit replication)

New repositories added to the mirror after that date are created as normal repository inside the project, with the gerrit replication plugin on replicating not only to but also to github.

This setup can be configured by us as github users, and we don't require manual action from github staff for it.

It works like follows:
  • gerrit replication plugin configuration (global, no repository-specific config required)
  • gerrit SSH public key configured as part of the "osmocom-gerrit" user at github
  • github user "osmocom-gerrit" part of the "osmoocm/bots" Team at github
  • github repositories having "write" permission for the "osmocom/bots" Team (and for safety nobody else)
To add a new repository "foo" to this setup, you need:
  • a repository
  • a repository (same name "foo" on both osmocom and github!)
    • give the "osmocom/bots" team (contains osmocom-gerrit user) write access to that repository
    • add a "Mirror from git://" description text
    • disable any of the "Projects/Wiki/Issues/..." features we don't use at github

After a few minutes, you should see replication to kick in and the branches/tags show up at github

Updated by laforge about 4 years ago · 2 revisions

Add picture from clipboard (Maximum size: 48.8 MB)