On Mon, Mar 02, 2020 at 09:30:08AM +0000, John Garry wrote:

> Do you want me to do anything about the above superfluous newline?

Whatever you prefer, I don't really care either way.