Page MenuHomePhabricator

[Task] Delete mediawiki/extensions/DataTypes from Gerrit
Closed, DuplicatePublic

Description

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.

Event Timeline

hashar created this task.Mar 19 2015, 8:20 AM
hashar raised the priority of this task from to Normal.
hashar updated the task description. (Show Details)
hashar added projects: Wikidata, DataTypes, Gerrit.
hashar added a subscriber: adrianheine.
Restricted Application added a subscriber: Aklapper. · View Herald TranscriptMar 19 2015, 8:20 AM

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.

Lydia_Pintscher changed the task status from Open to Stalled.Mar 19 2015, 9:58 AM
Lydia_Pintscher added a subscriber: Lydia_Pintscher.

Let's wait please and minimize the drama.

JanZerebecki moved this task from incoming to hold on the Wikidata board.May 16 2015, 10:45 PM

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.

Addshore renamed this task from Delete mediawiki/extensions/DataTypes from Gerrit to [Task] Delete mediawiki/extensions/DataTypes from Gerrit.Aug 14 2015, 8:05 AM
Addshore set Security to None.

I clearly said to wait. Why has T108457 been opened instead and the repo been deleted anyway? I am not saying this for fun.