On Thu, 19 Oct 2017 19:59:40 +1100 (AEDT), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote: > Do people think this is a cost worth paying? My answer is "yes". I haven't seen any replies to this post yet. I plan to commit a diff implementing my proposal tomorrow; you have until then to lodge any objection. Zoltan.