Yes, that looks like a copy/paste error indeed.
Thank you for reporting this.

Andi..