Fix a spelling mistake in a comment. NFC

(I'm currently trying to debug a strange error message I get when
pushing to github, despite the pushes being successful).