1 files changed, 0 insertions, 25 deletions

diff --git a/tools/run_tool.sh b/tools/run_tool.sh
deleted file mode 100755
index 2216a66..0000000
--- a/tools/run_tool.sh
+++ /dev/null
@@ -1,25 +0,0 @@
-#!/bin/sh
-
-if [ -z "$TOOL" ]; then
-        echo "No tool selected (TOOL variable must be set)"
-        exit 1
-fi
-
-CC="$CC -D_POSIX_C_SOURCE=199309L" # For timer
-
-BIN="tools/run"
-d="$(date +'%Y-%m-%d-%H-%M-%S')"
-
-for t in tools/*; do
-        if [ ! -d "$t" ] || ! (echo "$t" | grep -q "$TOOL"); then
-                continue
-        fi
-        toolname="$(basename "$t" .c)"
-        $CC -o $BIN "$t"/*.c "$CUBEOBJ" || exit 1;
-        $BIN $TOOLARGS \
-                | tee "tools/results/$toolname-$d.txt" "tools/results/last.out"
-        break
-done
-
-# $BIN is kept so it can be run manually for profiling
-rm -rf "$CUBEOBJ"