Re #6577. Trying to fix develop.

This file has gone missing on develop for some reason, though only
some build servers appear to care.