diff options
| author | David Bremner <david@tethera.net> | 2019-03-19 20:50:28 -0300 |
|---|---|---|
| committer | David Bremner <david@tethera.net> | 2019-03-19 20:54:15 -0300 |
| commit | 0557c5a0333b971188c02c961dec88496f2eed0c (patch) | |
| tree | 5af5a836cbdcddd6505e305d12e094802fd6351c /doc | |
| parent | 5569e042315862bdedb341472160cd09f4a0a2f7 (diff) | |
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.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile.local | 2 |
1 files changed, 1 insertions, 1 deletions
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. |