Fix a minor problem, and a little tidying.