Hi Jack,

thank you for the bug report, the analysis, and the patch.  I changed
the commit log and pushed it to the master branch with commit
579d17b70dac067f8194ede46513400b91ac136a.

Thanks!

--
Ricardo




Reply via email to