Merge "Revert "Move CSS for patrol from mediawiki.legacy to new module mediawiki...
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Thu, 11 Aug 2016 23:05:06 +0000 (23:05 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Thu, 11 Aug 2016 23:05:06 +0000 (23:05 +0000)
commit501d34c5995b67111d527828946f2a6ed7709849
tree839d197cdcde9c4b8497ac26e62addeb2127a67e
parentb664350b0b649d6214712ff87678aaaf8a7f2f9a
parent7cea81b8ffa5c7b58793e75850f1ee0d8f019ab7
Merge "Revert "Move CSS for patrol from mediawiki.legacy to new module mediawiki.page.patrol""
includes/diff/DifferenceEngine.php
resources/Resources.php
resources/src/mediawiki.legacy/shared.css