From 62591bedc8a32a67e6727008057ff0c10dc34d15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C8=98tefan=20Talpalaru?= <stefantalpalaru@yahoo.com>
Date: Thu, 10 Dec 2020 22:06:30 +0100
Subject: [PATCH] play nice with a parent Make

---
 run_nbc_benchmarks.sh | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/run_nbc_benchmarks.sh b/run_nbc_benchmarks.sh
index 3edd1ae..22b071f 100755
--- a/run_nbc_benchmarks.sh
+++ b/run_nbc_benchmarks.sh
@@ -20,6 +20,17 @@ else
 	GETOPT_BINARY="getopt"
 fi
 
+if uname | grep -qiE "mingw|msys"; then
+  # Windows
+  MAKE_CMD=mingw32-make
+else
+  MAKE_CMD=make
+fi
+
+if [[ -z "${MAKE}" ]]; then
+  MAKE=${MAKE_CMD}
+fi
+
 # argument parsing
 ! ${GETOPT_BINARY} --test > /dev/null
 if [ ${PIPESTATUS[0]} != 4 ]; then
@@ -89,7 +100,7 @@ if [[ -f "research/state_sim.nim" ]]; then
 	BENCHMARKS+=( state_sim )
 fi
 
-make -j${NPROC} NIMFLAGS="-f" ${BENCHMARKS[*]}
+"${MAKE}" -j${NPROC} NIMFLAGS="-f" --no-print-directory ${BENCHMARKS[*]}
 
 if [[ ${OUTPUT_TYPE} == "jenkins" ]]; then
 	OUT_DIR="."