Possibly we should have a CI job to check that this file is kept up to
date, but let's not do that now.

I filed #1484.