<div dir="ltr">How's this?<div><br></div><div><br></div><br><div class="gmail_quote"><div dir="ltr">On Tue, 20 Sep 2016 at 21:29 Thomas Lange <<a href="mailto:lange@informatik.uni-koeln.de">lange@informatik.uni-koeln.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">>>>>> On Tue, 20 Sep 2016 11:36:41 +0000, Paul Schulz <<a href="mailto:paul@mawsonlakes.org" target="_blank">paul@mawsonlakes.org</a>> said:<br>
<br>
    > Can this be put into the documentation somewhere?<br>
Do you have a patch for this?<br>
--<br>
regards Thomas<br>
</blockquote></div></div>