[patch] Share options between info and man page

[Eli Zaretskii]

> Date: Tue, 08 Jul 2014 10:47:37 +0100
> From: Pedro Alves <palves@redhat.com>
> CC: mingjie.xing@gmail.com, gdb-patches@sourceware.org
> 
> >  On top of that, this
> > whole "produce man pages from Texinfo" business was sold to us on the
> > assumption that "it makes maintenance simpler" (see
> > https://sourceware.org/ml/gdb-patches/2013-02/msg00290.html and the
> > discussions around it).  To me this means that we put a bunch of
> > telltale markers into the Texinfo files, add a few Makefile rules, and
> > promptly forget everything we knew about that.
> > 
> > But now it sounds like this arrangement is not simple at all, that we
> > need non-trivial changes to follow (which will probably stump someone
> > at some point, and perhaps even be changed and break the man-page
> > generation), we need to maintain texi2pod.pl, and whatnot else.
> 
> I found some documention on texi2pod.pl here:
> 
>  https://gcc.gnu.org/onlinedocs/gccint/Man-Page-Generation.html
> 
> Sounds like we actually want '@table @gcctabopt'.
> 
> > So I'm beginning to doubt that this is for the better.
> 
> I think the benefits once this is in place outweigh the hurdle we're
> going through.  I'd rather have a synced man page with the occasional
> odd formatting (that gets fixed eventually) than having to keep
> the two texts in sync manually.

In that case, if everyone else is happy with the patch, please approve
it, and let's see what happens next.