The mediawiki/extensions/DataTypes.git repo has been migrated to GitHub and should now be deleted.
Some context on T63601 , in short: we still maintain the Jenkins jobs for the repo which is rather useless.
Description
Description
| Status | Subtype | Assigned | Task | ||
|---|---|---|---|---|---|
| Resolved | Paladox | T62619 All repositories should pass jshint test | |||
| Invalid | adrianheine | T63601 DataTypes should pass jshint | |||
| Invalid | None | T108946 [Epic] Improve the development infrastructure | |||
| Duplicate | None | T93171 [Task] Delete mediawiki/extensions/DataTypes from Gerrit |
Event Timeline
Comment Actions
Doesn't this conflict with T74907: [Task] move git repositories that are dependencies of wikidata to gerrit?
Comment Actions
It does, but the ticket you linked is far from being decided. Depending on whether you prefer a) doing possibly unnecessary work or b) having a bit of cruft you can either do this or wait for T74907 to be resolved.
Comment Actions
What drama? Is anyone intent on keeping this obsolete copy of the repo around? Cleaning that up has no impact on what we can decide with regard to where we want to host things in the future.
Comment Actions
I clearly said to wait. Why has T108457 been opened instead and the repo been deleted anyway? I am not saying this for fun.