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

[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 locally before pushing.

Thanks,
  Stefano