patch for gdb.texinfo

[Dmitry Sivachenko]

> > By the way, this looks odd.  If everybody think that new commands
> > (@env and @command, in our case) are useless, we should write to
> > authors of texinfo and discuss it there.
>
> These new commands are not useless, they were introduced for very good
> reasons.
>
> What I was questioning was not the commands themselves, but the
> complete replacement of @code/@samp into @env/@option in the GDB
> manual, just because the new commands are there.  AFAIK, no other GNU
> manual has done such a total replacement.  Even the docs of the
> Texinfo package itself does not replace the old commands with the new
> ones, although in that case, you could say that there's no reason why
> it shouldn't: after all, the docs are generated when the package is
> built (Texinfo is special in this aspect), so the new features are
> *guaranteed* to be supported.
>
> I think the transition should be somewhat slower.  My experience
> suggests that back-compatibility is important, and should be broken
> only when necessary.  In this case, it is not necessary (IMHO).

Oh, well, I don't mind...

BR,
dima