(\indexfonts): Make leading be 12pt. Otherwise, it's too crammed.
authorKarl Berry <karl@gnu.org>
Mon, 29 Jul 1996 19:08:10 +0000 (19:08 +0000)
committerKarl Berry <karl@gnu.org>
Mon, 29 Jul 1996 19:08:10 +0000 (19:08 +0000)
commitbc60d5ea766c536db7925290efb9f682e9f49e21
treec88ae7de3925fcf615249f63f8de6bda58761f7a
parent1e0e41d2317391bdccaff26d9d8ea01201f06409
(\indexfonts): Make leading be 12pt. Otherwise, it's too crammed.

(\smalllispx): Remove \setleading{10pt}. That was too small.
(\doprintindex): Do not call \tex ... \Etex.  Index files are Texinfo
source, not TeX source, except for using \ instead of @ as the
escape character (for now).

From-SVN: r12573
gcc/texinfo.tex