Fix an old typo (a stray ; at the beginning of a line).