Actually in MediaWiki namespace: https://meta.wikimedia.org/wiki/MediaWiki:Gadget-WikiLabels.js
This makes deployments hard. We should specify that this task is done when we choose another place (or choose to leave it where it is.)
Ahha! I found that it was related to an incident. https://wikitech.wikimedia.org/wiki/Incident_documentation/20160531-wikilabels
So yeah, we're moving away from running WikiLabels as a gadget at all. That's why this is no longer valid.