doc/build: use $(MAKE) instead of make

This should silence some warnings about the jobserver, but also make
it easier to build the docs where GNU make is called something other
than make.

Based on a patch from aidecoe.

diff --git a/doc/Makefile.local b/doc/Makefile.local
index bab3d0d286ce75efe68433b3a8c82ab87eac7dd6..dfe62295d0965fed478a75d06361ca123ae934bc 100644 (file)
--- a/doc/Makefile.local
+++ b/doc/Makefile.local
@@ -56,7 +56,7 @@ sphinx-texinfo:
        $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(DOCBUILDDIR)/texinfo
 
 sphinx-info: sphinx-texinfo
        $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(DOCBUILDDIR)/texinfo
 
 sphinx-info: sphinx-texinfo

-       make -C $(DOCBUILDDIR)/texinfo info
+       $(MAKE) -C $(DOCBUILDDIR)/texinfo info

 
 # Use the man page converter that is available. We should never depend
 # on MAN_ROFF_FILES if a converter is not available.
 
 # Use the man page converter that is available. We should never depend
 # on MAN_ROFF_FILES if a converter is not available.