Today I have reported a bug at bug-autom...@gnu.org (see bug #43683 <https://debbugs.gnu.org/cgi/bugreport.cgi?bug=43683> – please use this link <https://debbugs.gnu.org/cgi/bugreport.cgi?msg=5;att=1;bug=43683> for a better rendering of the HTML). However I have written in the meanwhile a patch that solves the problem, and I guess this is the place where to submit it. Please find it attached.
--madmurphy
patch.tar.xz
Description: application/xz