From cb62076f8c5f0ea56dabb154912949e63ba59e9e Mon Sep 17 00:00:00 2001
From: ISSOtm <eldredhabert0@gmail.com>
Date: Fri, 6 Mar 2020 18:15:32 +0100
Subject: [PATCH] Use `$(MAKE)` instead of `make` in `develop`

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 4829822d..6a30df1a 100644
--- a/Makefile
+++ b/Makefile
@@ -210,7 +210,7 @@ wwwman:
 # compilation and make the continous integration infrastructure return failure.
 
 develop:
-	$Qenv make -j WARNFLAGS="-Werror -Wall -Wextra -Wpedantic \
+	$Qenv $(MAKE) -j WARNFLAGS="-Werror -Wall -Wextra -Wpedantic \
 		-Wno-sign-compare -Wformat -Wformat-security -Wformat-overflow=2 \
 		-Wformat-truncation=1 -Wformat-y2k -Wswitch-enum -Wunused \
 		-Wuninitialized -Wunknown-pragmas -Wstrict-overflow=5 \