However, neither in this mail, nor in your original did I find a
    corresponding patch.

Hi Jim - they ended up with separate bug#s, since separate emails.
At least I think these are those:
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=59992 (applied by mike?)
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=59993

BTW, see also the next bug,
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=59994
for more from Frederic, about flex madness.

karl