Page MenuHomePhabricator

Clone gerrit repo mediawiki/extensions/JADE to mediawiki/extensions/Jade
Closed, ResolvedPublic

Description

We're renaming the extension to Extension:JADE.

We have Diffusion and Github mirrors of this repo, those should be carried over to the new name by either moving or cloning.

Event Timeline

According to https://gerrit.wikimedia.org/r/Documentation/intro-project-owner.html#project-rename Gerrit core does not support the renaming of projects.

We could create a new repo, export everything from JADE and import it back to Jade; or

Install the rename-project plugin on Gerrit to do it (T201953).

I'm mentioning here @Paladox for advice.

We should create a new repo for now, since the rename plugin does not support NoteDB yet.

Halfak triaged this task as Medium priority.Feb 26 2019, 10:29 PM

I created the repo, trying to push all of the refs to it is giving me trouble though

When importing a repo I usually do:

  • git clone --bare ssh://$repo_clone_url
  • git push --mirror ssh://$repo_dest_url

This needs the forge-author-id, forge-commit-id and push privs granted to the Gerrit Managers in the repo though.

ok I pushed all of the refs, I think it should be identical now

Looks good from a quick coup d'œil. Now they have to stop committing to JADE and continue on Jade.

Should I lock and archive the old extension?

Yes it should be archived (and not deleted since we would lost changes and reviews made to it).

Projects-Cleanup has a link on the side bar Fill an archive request which comes with a long list of steps necessary to properly archive the extension. Tasks are typically handled by several volunteers (yeah!!).