Re: [PATCH] docs: mention $MAKE during configure

On 01/03/2013 10:54 PM, Eric Blake wrote:
> Based on a suggestion from Bob Friesenhahn:
> https://lists.gnu.org/archive/html/bug-automake/2013-01/msg00017.html
> 
> * doc/install.texi (Defining Variables): Mention that MAKE
> can be overridden, and the caveats that come with setting it.
> ---
> 
> How does this look?
> 
>  doc/install.texi | 10 +++++++++-
>  1 file changed, 9 insertions(+), 1 deletion(-)
> 
> diff --git a/doc/install.texi b/doc/install.texi
> index 4c2ffb5..bb08786 100644
> --- a/doc/install.texi
> +++ b/doc/install.texi
> @@ -5,7 +5,7 @@
> 
>  @unnumbered Installation Instructions
> 
> -Copyright @copyright{} 1994-1996, 1999-2002, 2004-2012 Free Software
> +Copyright @copyright{} 1994-1996, 1999-2002, 2004-2013 Free Software
>  Foundation, Inc.
> 
>  Copying and distribution of this file, with or without modification, are
> @@ -371,6 +371,14 @@ Defining Variables
>  CONFIG_SHELL=/bin/bash ./configure CONFIG_SHELL=/bin/bash
>  @end example
> 
> +Another variable to be aware of is @env{MAKE}; many packages allow this
> +to be set during @command{configure} in order to request the use of an
> +alternative @command{make} implementation (such as GNU make, which is
> +often present as @command{gmake}).  However, once an alternative is
> +chosen, the resulting Makefile may no longer work with the generic
> +@command{make}, so you must make sure to consistently use your
> +alternative make.
> +
s/make/@command{make}/?

Apart from that possible nit, ACK from me.

Thanks,
  Stefano