On 12/04/17 12:13, Andrew Dinn wrote: > Since these are tiny changes I am simply posting a git diff. Can someone > in the project team apply them and push them to the main repo? Or do I > have to provide a git PR? It's conventional to do that. I think it gets easier with time. Andrew.