make metrics uses the program in scripts/metricsgens to produce metrics.gen.go files from metric.go files. If the companion metrics.gen.go is not produced or updated, the new or updated metrics on metrics.go have no effect.

We should thus have a CI check to make sure that metrics.gen.go files are updated when metric.go files are changed.