aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorBen Gamari <ben@smart-cactus.org>2016-05-14 09:52:25 +0200
committerBen Gamari <ben@smart-cactus.org>2016-05-14 09:57:51 +0200
commit26e6b39de3213969d7de7f8bb3d4a849136866d1 (patch)
treedfd9874eb75556a3671cfb357f6bab695bb4d5f0 /doc
parent2904561d536908ab4d056cff41d707a88e21556c (diff)
doc: Use `$(MAKE)` instead of `make`
This is necessary to ensure we use gmake.
Diffstat (limited to 'doc')
-rw-r--r--doc/ghc.mk2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/ghc.mk b/doc/ghc.mk
index 3e53168e..afa3f078 100644
--- a/doc/ghc.mk
+++ b/doc/ghc.mk
@@ -19,6 +19,6 @@ INSTALL_HTML_DOC_DIRS += utils/haddock/doc/haddock
endif
html_utils/haddock/doc :
- make -C utils/haddock/doc html SPHINX_BUILD=$(SPHINXBUILD)
+ $(MAKE) -C utils/haddock/doc html SPHINX_BUILD=$(SPHINXBUILD)
cp -R utils/haddock/doc/.build-html utils/haddock/doc/haddock