OSDN Git Service

(\indexfonts): Make leading be 12pt. Otherwise, it's too crammed.
authorkarl <karl@138bc75d-0d04-0410-961f-82ee72b054a4>
Mon, 29 Jul 1996 19:08:10 +0000 (19:08 +0000)
committerkarl <karl@138bc75d-0d04-0410-961f-82ee72b054a4>
Mon, 29 Jul 1996 19:08:10 +0000 (19:08 +0000)
commit7e8abc9e4e0effbc0e4d8f71296a7706dd8ca85f
treec88ae7de3925fcf615249f63f8de6bda58761f7a
parent580ee5be89291eca74be9b678f300608647edcbb
(\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).

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@12573 138bc75d-0d04-0410-961f-82ee72b054a4
gcc/texinfo.tex