Merge pull request #25 from h0nzZik/fix-missing-dep

fix build-and-profile
h0nzZik · Jun 30, 2024 · be1776a · be1776a
2 parents eff132b + 405cf37
commit be1776a
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/bench-coq/build-and-profile.sh b/bench-coq/build-and-profile.sh
@@ -1,5 +1,12 @@
 #!/usr/bin/env bash
 
+set -e
+
+# https://stackoverflow.com/a/246128/6209703
+SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
+
+pushd "$SCRIPT_DIR" > /dev/null
+
 TIME=$(which time)
 
 # https://stackoverflow.com/a/10983009/6209703