Fixup for Coverity issue #101137.