Merge branch 'dev'

1 files changed, 3 insertions, 8 deletions

diff --git a/local-tomo b/local-tomo
index 76864837..d16e090e 100755
--- a/local-tomo
+++ b/local-tomo
@@ -1,11 +1,6 @@
 #!/bin/sh
 version=$(awk '/^## / {print $2; exit}' CHANGES.md)
-here="$(realpath "$(dirname "$0")")"
-if [ ! -e "$here/build/bin/tomo@$version" ]; then
-    echo "Tomo hasn't been compiled yet! Run \`make\` to compile it!"
-    exit 1;
+if ! [ -e ./build/$version/bin/tomo ]; then
+    make -j
 fi
-
-PATH="$here/build/bin${PATH:+:$PATH}" \
-TOMO_PATH="$here/build" \
-tomo@"$version" "$@"
+exec ./build/$version/bin/tomo "$@"