> Shouldn't you use @documentencoding if you include UTF-8 encoded
> characters verbatim?  (I have no idea if that affects the problem.)

UTF-8 is meanwhile the default encoding.


    Werner

Reply via email to