Issue description: https://rt.psg.com/Ticket/Display.html?id=1555 This seems purely editorial and attracted no discussion, so I suggest closing it and leaving it to the editors to take it or leave it. If no one objects, I'll ask Eliot to close this on July 11th. S.