Ah, thank you. Yes, you’re right, that was just a paste-buffer error. I just checked in the fix.
David