Thanks for the quick fix! Best, Antoine On 10 Jun 2017 10:25 am, "Eli Zaretskii" wrote: > Date: Mon, 05 Jun 2017 19:20:41 +0300 > From: Eli Zaretskii > Cc: 27243@debbugs.gnu.org, antoine.levitt@gmail.com > > > Your fix is certainly simpler and I think cleaner than mine, so I would > > say install it. > > OK, thanks. I will wait for a couple of days to let others a chance > to chime in, and will install if no further comments come up. No further comments, so I pushed the change, and I'm marking this bug done.