even more fixes from randomconfig runs

1 file changed