<?php // This was an old reindexing migration that has been obsoleted. See T13253.