On Fri, May 04, 2018 at 07:54:46PM +0100, Chris Lamb wrote: > How did you get on with this? :) No. I was pondering it on irc and it didn't seem immediately actionable to me. You wanted a bug report anyway and you got one. Is there really much point in discussing whether tool diversity is good? The case seems pretty clear to me. Helmut