From a85f4cc1699e594d170075a57c98797a51e62617 Mon Sep 17 00:00:00 2001
From: Antonin Portelli <antonin.portelli@me.com>
Date: Thu, 26 Jan 2023 18:57:47 +0000
Subject: [PATCH] better Grid bench build script

---
 Grid/build-benchmark.sh | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Grid/build-benchmark.sh b/Grid/build-benchmark.sh
index 4b973d5..92ce696 100755
--- a/Grid/build-benchmark.sh
+++ b/Grid/build-benchmark.sh
@@ -16,18 +16,16 @@ cd "${env_dir}"
 env_dir=$(pwd -P)
 cd "${call_dir}"
 build_dir="${env_dir}/build/Grid-benchmarks/${cfg}"
-if [ -d "${build_dir}" ]; then
-    echo "error: directory '${build_dir}' exists"
-    exit 1
-fi
 mkdir -p "${build_dir}"
 source "${env_dir}/env.sh"
 entry=$(jq ".configs[]|select(.name==\"${cfg}\")" "${env_dir}"/grid-config.json)
 env_script=$(echo "${entry}" | jq -r ".\"env-script\"")
 cd "${build_dir}" || return
 source "${env_dir}/${env_script}"
-"${script_dir}/configure" --with-grid="${env_dir}/prefix/grid_${cfg}" \
-                          --prefix="${env_dir}/prefix/gridbench_${cfg}"
+if [ ! -f Makefile ]; then
+    "${script_dir}/configure" --with-grid="${env_dir}/prefix/grid_${cfg}" \
+                            --prefix="${env_dir}/prefix/gridbench_${cfg}"
+fi
 make -j 128
 make install
 cd "${call_dir}"