Robert de Bath's patch: be much more careful about font heights and