> Date: Mon, 05 Jun 2017 19:20:41 +0300
> From: Eli Zaretskii <eliz@gnu.org>
> Cc: 27243@debbugs.gnu.org, antoine.levitt@gmail.com
>No further comments, so I pushed the change, and I'm marking this bug
> > 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.
done.