On Thu, Aug 9, 2018 at 6:51 PM, Alexander Ploumistos <
alex.ploumistos(a)gmail.com> wrote:
On Fri, Aug 10, 2018 at 12:41 AM Jeff Backus
<jeff.backus(a)gmail.com>
wrote:
> Quick update: I found the problem and put together a patch (see BZ).
I'll work on submitting the fix to upstream next week.
Hats off to you sir!
Thanks! It was ... tedious. :)
--
Jeff Backus
jeff.backus(a)gmail.com
http://github.com/jsbackus