<div dir="ltr"><div class="gmail_extra">Sorry I didn't see this a few minutes ago. Rebased it myself against master, and merged. Thanks for your work on this. Looking forward to log-filter next!
</div></div>