Merge "Add Priority Hints support"
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Mon, 25 Feb 2019 20:31:59 +0000 (20:31 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Mon, 25 Feb 2019 20:31:59 +0000 (20:31 +0000)
commit227a807ef50387393df0641bce0a6cd16e550338
tree94a4d35bb076237d8fc414d2f73c7838d45cab38
parentcabf43cc00df3a858652c7515bce1b14696783d0
parent8e11c5dabc56f5bc0127054ae65735cbfcc62258
Merge "Add Priority Hints support"
includes/DefaultSettings.php