doc: Use `$(MAKE)` instead of `make`

This is necessary to ensure we use gmake.

2 files changed, 2 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 3875c3a2..d450cff5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,6 @@
 Changes in version 2.17.2
 
- * TODO
+ * Fix portability of documentation building within GHC
 
 Changes in version 2.17.1
 
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