<div dir="ltr">Hi Graham,<br><br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
</span>I can send you a diff or simply push the changes to git myself.<span class="HOEnZb"><font color="#888888"><br></font></span></blockquote><div><br></div><div>Both options are fine with me. If want to push the changes to git yourself, it eliminates double work, so you are very welcome :-).<br><br></div><div>Thanks!<br></div><div>Sebastian<br></div></div><br><br><div dir="ltr"><div><div dir="ltr"><div><font style="font-family:courier new,monospace" face="courier new,monospace"></font><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"></span></div></div></div></div>
</div></div>