GNU make version

[Norbert Thiebaud]

I just ran a make no-op (a make on a fully built product, which
presumably should expose the performance of make itself more than
anything else)
on a Windows VM, using _our_ 3.82 form dev-tools and _our_ 3.81 form dev-tools
the result are
3.82:  14m19.125  4m31.200 9m15.539
3.81:  14m20.618  4m39.261 9m12.333

iow. the whole thing about 3.82 is slow is unfounded. Stock 3.82 _is_
slow because there was a bug that has been found and patched, even
up-streamed by michael IIRC... and that was almost a year ago now...

I was amongst those that resisted the notion of having our own gnu
make forcibly bootstrapped in the build process, like we have dmake
now...
I do not object to a --build-make or something like that in
configure.in to automate the building of our own gmake... at least
until the situation settle upstream
_but_ any such version we optionally build from configure _must_ be
straight-up compatible with upstream. we cannot afford to start having
Makefile that
_require_ a custom gnu-make to build.

Norbert