People normally use cut&paste, and that often adds unexpected white space
characters. So we simply remove them for convenience.