<div dir="ltr">On further thought, I found that we never need to merge groups, so there<div>are no bug here.</div><div><br></div><div>-- Andrey Khalyavin<br><div><div class="gmail_extra"><br><div class="gmail_quote">2014-12-04 21:56 GMT+03:00 Andrey Khalyavin <span dir="ltr"><<a href="mailto:halyavin@google.com" target="_blank">halyavin@google.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This patch only makes algorithm clearer. It doesn't fix the bug that<br>
groups may need to be merged as they became more general.<br>
<br>
-- Andrey Khalyavin<br>
<br><span class="HOEnZb"><font color="#888888"><br>
</font></span></blockquote></div><br></div></div></div></div>