Merge pull request #1036 from stan-dev/update-make-command

Use `$MAKE` if set, otherwise fall back to system specific `make` command
stan-dev · Nov 22, 2024 · c681d32 · c681d32
2 parents 4b80205 + 73a1cb2
commit c681d32
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/R/utils.R b/R/utils.R
@@ -92,8 +92,11 @@ arch_is_aarch64 <- function() {
 }
 
 # Returns the type of make command to use to compile depending on the OS
+# First checks if $MAKE is set, otherwise falls back to system-specific default
 make_cmd <- function() {
-  if (os_is_windows() && !os_is_wsl() && (Sys.getenv("CMDSTANR_USE_RTOOLS") == "")) {
+  if (Sys.getenv("MAKE") != "") {
+    Sys.getenv("MAKE")
+  } else if (os_is_windows() && !os_is_wsl() && (Sys.getenv("CMDSTANR_USE_RTOOLS") == "")) {
     "mingw32-make.exe"
   } else {
     "make"