Fix a typo reported by Juanjo on the user mailing list.