> In fact, in the es/maxima.texi file there is a line with the
> following contents:
>
> @documentencoding ISO-8859-1
I put that into the Spanish and Portuguese texinfo files
a long time ago because it seemed necessary to get
diacriticals to appear correctly. Perhaps I was mistaken about that.
I don't really know much about character encoding.
Robert