Re: [committed] Fix gdb.texinfo for old makeinfo (again)

Eli Zaretskii
2018-01-15T12:12:57Z

> Date: Mon, 15 Jan 2018 11:51:52 +0000
> From: Szabolcs Nagy <szabolcs.nagy@arm.com>
> CC: nd@arm.com, Sergio Durigan Junior <sergiodj@redhat.com>, Simon Marchi <simon.marchi@polymtl.ca>, Tom Tromey <tom@tromey.com>, Eli Zaretskii <eliz@gnu.org>
> now with patch attached.

Hmm... why did you need this one:

> -@pindex gdb-add-index

That's an index entry for gdb-add-index, it should stay, I think.