The attached series of patches should fix bug #55719 (https://debbugs.gnu.org/cgi/bugreport.cgi?bug=55719).

I have already signed the copyright assignment agreement.

Thanks,
Richard