Apologies -- I selected the wrong commit to extract the commit messagefrom. Here it is again. I also removed an obsolete /* XXX */ comment.
-- Álvaro Herrera Breisgau, Deutschland — https://www.EnterpriseDB.com/