<?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.