2018-09-03 - releng
08:21	<Hauskatze>	github: added "this is a mirror" notice (as nearly all other repos have) to https://github.com/wikimedia/mediawiki-extensions-UserExport	[releng]