[fix] Makefile: Use $(MAKE) instead of hardcore "make".

MLstate · Apr 10, 2012 · 3e3c2e6 · 3e3c2e6
1 parent 7e413a8
commit 3e3c2e6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -36,7 +36,7 @@ export
 all: $(MYOCAMLBUILD)
 	$(OCAMLBUILD) $(call target-tools,$(ALL_TOOLS)) opa-packages.stamp
 	@$(call copy-tools,$(ALL_TOOLS))
-	make manpages
+	$(MAKE) manpages
 
 .PHONY: build
 build: all