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