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.
This commit is contained in:
David Bremner 2019-03-19 20:50:28 -03:00
parent 5569e04231
commit 0557c5a033

View file

@ -56,7 +56,7 @@ 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.