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

[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.