Re: Makefile.maint (Was: TODO)

[Tim Van Holder]

> Index: .prev-version
Minor nit, but could this be a more dos-friendly name (no leading dot
supported)?

> +# Systems where /bin/sh is not the default shell need this.  The $(shell)
> +# command below won't work with e.g. stock DOS/Windows shells.
> +SHELL = /bin/sh

This sounds a bit like the $(shell) command doesn't work on DOS/Windows
due to/regardless of the setting of SHELL.  On DJGPP, at least, this
is not true - setting SHELL like this ensure unixy commands work just
fine in a makefile (only when SHELL isn't set in a makefile does make
default to the broken DOS command interpreter).
So perhaps

   # Systems where /bin/sh is not the default shell need this.  This is
   # especially needed on DOS/Windows, where the $(shell) command below
   # wouldn't work with the stock shell.

would be more appropriate.  I don't know if this would apply to Cygwin as
well, but I would think it odd if having SHELL=/bin/sh broke its make.