(\indexfonts): Make leading be 12pt. Otherwise, it's too crammed.
authorkarl <karl>
Mon, 29 Jul 1996 19:08:10 +0000 (19:08 +0000)
committerkarl <karl>
Mon, 29 Jul 1996 19:08:10 +0000 (19:08 +0000)
commit8fa294a31d38c2a6d4696a7b6935f1effd72edc2
tree8e7174e98170e8cc9d4e89f996c4bd90040615fc
parente76a4844ccd9d6db7d6027eec614ea07ef568e92
(\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).
manual/texinfo.tex