Page MenuHomePhabricator

Fix jade role in mediawiki vagrant
Closed, ResolvedPublic

Description

The mediawiki extension was renamed from JADE => Jade, which was not updated in the mediawiki vagrant repo.

This results in an incorrect version being provisioned.

See: https://gerrit.wikimedia.org/r/admin/projects/q/filter:jade

Event Timeline

ACraze created this task.Aug 28 2019, 9:11 PM
Restricted Application added a subscriber: Aklapper. · View Herald TranscriptAug 28 2019, 9:11 PM
ACraze updated the task description. (Show Details)Aug 28 2019, 9:15 PM

Change 533085 had a related patch set uploaded (by Accraze; owner: Accraze):
[mediawiki/vagrant@master] Updated jade role

https://gerrit.wikimedia.org/r/533085

Change 533085 merged by jenkins-bot:
[mediawiki/vagrant@master] Updated jade role

https://gerrit.wikimedia.org/r/533085

Halfak closed this task as Resolved.Sep 17 2019, 2:56 PM