>> So we now encourage not to use @documentencoding at all if it's UTF-8? > > Indeed.
It doesn't sound to my ears that the manual 'encourages' to not tag a
file with `@documentencoding`. However, it is no longer necessary
since more than five years.
Werner
