another fix for build failure found by randomconfig

1 file changed