Hi,

Please close this. I added a patch series to 
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=38689

Thanks,
Alex