Work around a build problem on Debian Buster.