On 10/11/16 20:15, Doug Simon wrote: > We should move discussion of this patch to the github pull request once it exists. OK. My experience of github (and indeed git) is basically zero, so you'll need to have some patience with me. Andrew.