@documentencoding, `makeinfo --enable-encoding' (was: Syncing some doc fixes to v5-10)

[Reiner Steib]

On Tue, Sep 21 2004, Jesper Harder wrote:

> Miles Bader <address@hidden> writes:
>
>> Jesper Harder <address@hidden> writes:
>>
>>> Is it strictly necessary?  It doesn't really matter except for the
>>> hard-copy version.  And I'd rather not mess around with the Emacs
>>> Make/Automake files (which would be required).
>>
>> Are these changes that would be desirable in general for the emacs doc
>> Makefiles?
>
> I don't know ... if the Emacs docs contain many Texinfo-"encoded"
> Latin-1 chars, e.g. @aa{} and so on, I suppose it would be nicer to
> display them with the actual glyph, "å", rather than in an ASCII
> rendition, "aa".

Beside `gnus.texi', there are some other files in Emacs using
non-ascii characters (this list is most probably incomplete):

--8<---------------cut here---------------start------------->8---
emacs/man$ grep -ie '[äöüßáéíóúàèìòù¬]' -e '@aa{}' -e '@\"[aou]' *.texi
ack.texi:Torbj@"orn
emacs.texi:Dukhovni, John Eaton, Rolf Ebert, Stephen Eglen, Torbj@"orn 
Einarsson,
emacs.texi:Sebastian Kremer, Geoff Kuenning, David address@hidden, Daniel 
LaLiberte,
faq.texi:Roland Schäuble reports that Emacs 18.58 running on plain TOS and MiNT
gnus.texi:makes strings like @samp{déjà vu} look like @samp{d=E9j=E0 vu}, which
gnus.texi:@itemx ¬
ses.texi:Stefan Reichör @email{xsteve@@address@hidden
--8<---------------cut here---------------end--------------->8---

It becomes quite obvious that something is wrong when you look at the
info pages using...

LC_ALL=greek emacs -q -no-site-file --eval '(info "(efaq)Emacs for Atari ST")'

... or similar: You get "Schδuble" instead of "Schäuble".

IIRC, at least Latin-1 characters work correctly in info and dvi when
using --enable-encoding and @"a [1].

Bye, Reiner.

[1] 
http://search.gmane.org/search.php?group=gmane.comp.tex.texinfo.general&query=documentencoding+enable+encoding
-- 
       ,,,
      (o o)
---ooO-(_)-Ooo---  |  PGP key available  |  http://rsteib.home.pages.de/