1 files changed, 0 insertions, 40 deletions

diff --git a/tools/tool.sh b/tools/tool.sh
deleted file mode 100755
index aea203f..0000000
--- a/tools/tool.sh
+++ /dev/null
@@ -1,40 +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"
-RESULTS="tools/results"
-LAST="$RESULTS/last.out"
-date="$(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)"
-        break
-done
-
-file="$RESULTS/$toolname-$date.txt"
-
-$CC -o $BIN "$t"/*.c "$OBJ" || exit 1;
-
-(
-date +'%Y-%m-%d %H:%M'
-echo ""
-echo "======== config.mk ========"
-cat config.mk
-echo ""
-echo "=== tool configuration ===="
-echo "TOOL=$toolname"
-echo "TOOLARGS=$TOOLARGS"
-echo "CC=$CC"
-echo ""
-echo "======= tool output ======="
-$BIN $TOOLARGS 
-) | tee "$file" "$LAST"