(\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)
commitbcd11d854bcc3c1d7a661dbb20f219694ff48492
treeb5d2a33eab127c7d27f4a35f48fc56acf5600c01
parentbb01a1a810a03046c05b757c2c88d98651f5e452
(\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).
texinfo.tex