play nice with a parent Make

This commit is contained in:
Ștefan Talpalaru 2020-12-10 22:06:30 +01:00
parent 8b767d8b6d
commit 62591bedc8
No known key found for this signature in database
GPG Key ID: CBF7934204F1B6F9

View File

@ -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="."