<div dir="ltr"><div class="gmail_extra">Just want to make sure the pull request is noticed.</div><div class="gmail_extra">The proposal is ready for merge. Note that we can now &quot;squash and merge&quot; on Github.</div><div class="gmail_extra"><br></div><div class="gmail_extra">- Anton</div></div>