Correct horrible error accidentally left in previous commit (this message genuine as previous commit with spurious message was a slip of the fingers...).
