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> (may not be visible to non-Wikimedians, sorry), the WebHook receiver < http://tools.wmflabs.org/suchaserver/cgi-bin/receiver.py> 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