The Jade extension now has a repository at the "Jade" name.
When I go to https://github.com/wikimedia/mediawiki-extensions-Jade (note the lack of all-caps) it automatically points to https://github.com/wikimedia/mediawiki-extensions-JADE (note the all-caps).
@thcipriani @mmodell do you know what needs to happen for this change to take effect?
| Status | Subtype | Assigned | Task | ||
|---|---|---|---|---|---|
| Declined | None | T212435 Review real-world query plans and performance for Jade | |||
| Declined | None | T238877 Write Huggle labels to Jade | |||
| Declined | calbon | T183381 Deploy pilot of Jade to a small set of wikis. | |||
| Resolved | Reedy | T211046 Rename "JADE" extension to "Jade" | |||
| Resolved | hashar | T221436 GitHub should point to "Jade" and not "JADE" |
Github repository names are case insensitive as far as I can remember. See eg:
I have renamed the repository in Github to use Jade which is what used for display purposes ;]