On Thu, Mar 02, 2017 at 12:19:44PM +0100, Mike Belopuhov wrote: > Here's an updated diff with suggestions from bluhm@ and it's > even slimmer now but I don't mind either way. If David isn't > comfortable with this change, we don't have to do it.
OK bluhm@
