On Wed, 14 Oct 2020 at 21:05, David Rowley <dgrowleyml(at)gmail(dot)com> wrote:> I've attached the patch I ended up with. I plan on pushing this in the> next few days.
Pushed.
David