From 26e6b39de3213969d7de7f8bb3d4a849136866d1 Mon Sep 17 00:00:00 2001
From: Ben Gamari <ben@smart-cactus.org>
Date: Sat, 14 May 2016 09:52:25 +0200
Subject: doc: Use `$(MAKE)` instead of `make`

This is necessary to ensure we use gmake.
---
 doc/ghc.mk | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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
 
-- 
cgit v1.2.3