From 0557c5a0333b971188c02c961dec88496f2eed0c Mon Sep 17 00:00:00 2001 From: David Bremner Date: Tue, 19 Mar 2019 20:50:28 -0300 Subject: [PATCH 1/1] 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. --- doc/Makefile.local | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/Makefile.local b/doc/Makefile.local index bab3d0d2..dfe62295 100644 --- a/doc/Makefile.local +++ b/doc/Makefile.local @@ -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. -- 2.43.0