Karl Berry bc60d5ea76 (\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		1996-07-29 19:08:10 +00:00
gcc	(\indexfonts): Make leading be 12pt. Otherwise, it's too crammed.	1996-07-29 19:08:10 +00:00