Bugfix by Rob W. W. Hooft, from his spelling fixes patch. This one is a

genuine bug, so I checked it in separately.