2018-07-09 - releng
10:40	<hashar>	github: deleting https://github.com/wikimedia/mediawiki-extensions-ContributorsAddon | T198864	[releng]