Re: [PATCH] docs: mention dist-hook help for EXTRA_DIST

2013-01-03 Thread Stefano Lattarini
On 01/04/2013 12:11 AM, Karl Berry wrote: > I didn't mind taking 3 minutes to convert this into a git commit. > > Thanks. > >From me too. > +ameliorate the problem; @xref{The dist Hook}. > > I'm afraid that's the wrong kind of xref (capital See). Needs to be @pxref. > I've fixed that l

Re: [PATCH] docs: mention dist-hook help for EXTRA_DIST

2013-01-03 Thread Karl Berry
I didn't mind taking 3 minutes to convert this into a git commit. Thanks. +ameliorate the problem; @xref{The dist Hook}. I'm afraid that's the wrong kind of xref (capital See). Needs to be @pxref.