Subject: bug#25424:

From: Eli Zaretskii <[email-masked]>
Date: Fri, 22 Mar 2019 15:15:35 +0200

> From: Tijs Mallaerts <[email-masked]>
> Date: Fri, 22 Mar 2019 11:33:08 +0100
> 
> Could someone please verify if this patch is ok?

Sorry for the delay, CC'ing the relevant maintainer.

Michael, could you please look at the patch proposed in
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=25424#10?

Thanks.