I just stumbled across https://github.com/wikimedia/mediawiki-core/pull/19, a small but useful contribution to core from an HHVM developer. It has gone unnoticed for two months, which is a bit sad.
Is there a way to accept pull-requests from GitHub? According to < https://github.com/wikimedia/mediawiki-core/settings/hooks%3E (may not be visible to non-Wikimedians, sorry), the WebHook receiver < http://tools.wmflabs.org/suchaserver/cgi-bin/receiver.py%3E is defunct. Anyone know the story there?
It'd be good if some additional people were watching (that is, receiving notifications for) https://github.com/wikimedia/mediawiki-core/.
I haven't responded yet, by the way, so feel free to if you know the answers to these questions. I don't know what effect accepting the pull-request will have on the code in master, and telling someone who has already submitted a patch to go sign up for Gerrit seems impolite.
Ori