[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PATCH] docs: mention dist-hook help for EXTRA_DIST
|
From: |
Stefano Lattarini |
|
Subject: |
Re: [PATCH] docs: mention dist-hook help for EXTRA_DIST |
|
Date: |
Fri, 04 Jan 2013 01:09:47 +0100 |
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