From: David Bremner <david@tethera.net>
Date: Tue, 19 Mar 2019 23:50:28 +0000 (-0300)
Subject: doc/build: use $(MAKE) instead of make
X-Git-Tag: archive/debian/0.29_rc0-1~127
X-Git-Url: https://git.notmuchmail.org/git?p=notmuch;a=commitdiff_plain;h=0557c5a0333b971188c02c961dec88496f2eed0c

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 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.