<div dir="ltr"><div class="gmail_extra">I suppose it's possible, if people would have a strong preference, to fix the bug first and then refactor the code.</div><div class="gmail_extra">We could certainly check upon seeing the "/z7" flag whether a later-occurring option is stronger than it.</div></div>