Merge "Revert and fix "Revert "Modify -—with-extensions to throw extension dependency...
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Mon, 9 Sep 2019 20:05:01 +0000 (20:05 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Mon, 9 Sep 2019 20:05:01 +0000 (20:05 +0000)
commit93d9da40d3153ee8f63ffbd7bc72f08d62e11efd
tree6fedd5d4f013e35e08814fc478cfd47e795e1dd6
parentaf24fc1a7a52df5b5ad7157aa9d27b76c1a26ef4
parent0aec1401e59f0c386729792515995b319d6480e0
Merge "Revert and fix "Revert "Modify -—with-extensions to throw extension dependency errors"""