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/