Branching off from bug 35497, which is about setting up an easy-as-possible pull-request link to Gerrit once the mirror is set up
Version: unspecified
Severity: normal
Branching off from bug 35497, which is about setting up an easy-as-possible pull-request link to Gerrit once the mirror is set up
Version: unspecified
Severity: normal
Status | Subtype | Assigned | Task | ||
---|---|---|---|---|---|
Resolved | • demon | T24596 Migrate subversion to git | |||
Declined | None | T37497 Implement a way to bring GitHub pull requests into gerrit | |||
Resolved | None | T40196 Set up https://github.com/mediawiki/core mirror | |||
Resolved | • demon | T37429 Mirrors all git repositories to GitHub |
(Cite bug 35497 comment #13)
So, some ideas:
- Don't use github.com/mediawiki/core as name
- means we duplicate user groups/rights with the org "Wikimania" at github
- means we're going to promote ourselves as "core". e.g.
github.com/Krinkle/core.
- any advantages? hashar mentioned we want to be able to allow volunteers to help out with the
handling of pull-request and that to grant them rights we'd want to have it
outside the @wikimedia organization. However this is not needed because:
- github allows collaboration without any rights at all. You can leave
inline comments, and stuff on any pull request anywhere
- as in comment 12, they are pull-able in many different formats including
plain "git pull" so anyone can pull it locally, and if they have a labs ldap
account they can also push straight to gerrit for review.
- github supports auto-closing of pull-requests when the commit hash is
pushed into the repo, so no maintenance there either. And if the commit has to
be amended, including "fixes GH-123" or "closes GH-123" will also close the
relevant PR as soon as it is merged. And if all else fails, a repo collab in
@wikimedia (of which there are many[1]) can just push "Close" manually on
githubSo volunteers have complete access without needing to be manually added toanything, this is what made GitHub works. And if its only about closing some
exceptional ones, then I'm sure we'll manage that.
- Use github.com/wikimedia/mediawiki-core
- ideally we'd have some kind of auto-push from gerrit or jenkins, otherwise
just set up a 30 minute cron somewhere to pull gerrit -f and `push github
-f`.
- admin settings: pull-request: true, issues: false, wiki: false
How is this not a duplicate of bug 35429? I'll be doing all the repos at once when I setup replication, not one-by-one.
(In reply to comment #2)
How is this not a duplicate of bug 35429? I'll be doing all the repos at once
when I setup replication, not one-by-one.
I didn't say it wasn't a dupe. But since it appears there is no clarity yet on how the gerrit or jenkins replication is going, I figured we may be able to set up at least something on the short term for mediawiki-core so that its out there and we can start experimenting with how to solve other issues such as what and if we need a tool for pulling in pull-requests (or that git pull github.com...; git push gerrit HEAD:refs/for/master/gh-123/some-feature; is sufficient).
I mean.. I could just ask for the repo and set a cron up to mirror and get it going. Seems low hanging fruit. But if bug 35429 can be done within say 2 weeks, then by all means dupe it.