<?php
// A later patch ("20160510.repo.01.uriindex.php") performs an identical
// regeneration of the index, so we no longer need to do it here.