In T112120: [Task] Move ValueView repository from github to gerrit it was decided to use https://gerrit.wikimedia.org/r/#/admin/projects/data-values/value-view for the ValueView component, mirrored to https://github.com/wikimedia/data-values-value-view.
The old https://gerrit.wikimedia.org/r/#/admin/projects/mediawiki/extensions/ValueView still exists and is still mirrored to https://github.com/wikimedia/mediawiki-extensions-ValueView. Both is confusing.
| Status | Subtype | Assigned | Task | ||
|---|---|---|---|---|---|
| Resolved | hashar | T123624 [Task] Redirect unused extensions/ValueView repository to data-values/value-view | |||
| Resolved | JanZerebecki | T112120 [Task] Move ValueView repository from github to gerrit | |||
| Duplicate | None | T114649 delete mediawiki/extensions/ValueView from gerrit |
https://wikitech.wikimedia.org/wiki/Gerrit#Deleting_repositories tells to file this against Continuous-Integration-Infrastructure.
Change 264306 had a related patch set uploaded (by Chad):
Remove a couple of repositories from the meta repo
(1) is done. (2) and (3) seem to be opposites of one another. Do we want to redirect or delete outright?
Personally I very much prefer redirects because they do not leave people stuck in dead ends.
Change 264933 had a related patch set uploaded (by Hashar):
[ValueView] Delete untriggered Jenkins jobs
I have removed the extension from CI and deleted the related GitHub mirror which had no content beside the .gitreview file https://github.com/wikimedia/mediawiki-extensions-ValueView . No point in setting up a redirect since that repo was almost entirely empty and thus unlikely to have been linked / used.