https://bugzilla.wikimedia.org/show_bug.cgi?id=68054
Krinkle <[email protected]> changed: What |Removed |Added ---------------------------------------------------------------------------- Summary|Gerrit: Remove duplicate |Gerrit: Use GitHub |mirrors on GitHub |redirects instead of | |duplicate mirrors --- Comment #3 from Krinkle <[email protected]> --- The redirects GitHub has in place apply both to the HTTP protocol (web interface) as well as the Git interface itself. We can simply remove the duplicate "pretty name" replications and perform the renames on GitHub. That way there's only one repo Gerrit is pushing two and both urls work. I've gone ahead and done this with mediawiki-core as example. From Gerrit's perspective it's a straight up replication from gerrit:mediawiki/core to github:mediawiki-core. There is no fancy-name duplicate set up for it. On GitHub it has been renamed from mediawiki-core with a full redirect in place. Gerrit is now effectively pushing to https://github.com/wikimedia/mediawiki while all urls and logs for mediawiki-core continue to work as expected. -- You are receiving this mail because: You are the assignee for the bug. You are on the CC list for the bug. _______________________________________________ Wikibugs-l mailing list [email protected] https://lists.wikimedia.org/mailman/listinfo/wikibugs-l
