Pointers are all the same size, so it makes no practical difference, but
let's be tidy.

Found by Coverity, noted off-list by Tom Lane.