Thanks for that. I've submitted https://gerrit.wikimedia.org/r/#/c/117158/ to fix it, hopefully it will get merged sooner rather than later. If that happens sometime in the next ~12 hours it should be in time for 1.23wmf17, otherwise it'll have to wait for 1.23wmf18 or later (see https://www.mediawiki.org/wiki/MediaWiki_1.23/Roadmap for the schedules).