Minor fix (that would never actually occur).