Re: bug#16337: [PATCH] doc: fix encoding error with UTF-8 characters

[Paul Eggert]

Stefano Lattarini wrote:

please push (to the 'micro' branch) and close this bug
report once you're done

Thanks, done.