Hi Ludo, On Mon, 16 Sep 2019 at 10:17, Ludovic Courtès <[email protected]> wrote:
> Bonus points if you send the patch with ‘git format-patch’ and with a > commit log: I did my best here: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=37448 Hope I am doing right. Thanks, simon
