From 0557c5a0333b971188c02c961dec88496f2eed0c Mon Sep 17 00:00:00 2001
From: David Bremner <david@tethera.net>
Date: Tue, 19 Mar 2019 20:50:28 -0300
Subject: [PATCH] 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.