<?php // This previously updated the PROJ index, but HEAD can no longer reindex // old PROJ records properly (since fields have been added to various places) // and this migration is 6 months old and optional. Just skip it.