1 files changed, 22 insertions, 0 deletions

diff --git a/tools/tool.sh b/tools/tool.sh
new file mode 100755
index 0000000..64bfd89
--- /dev/null
+++ b/tools/tool.sh
@@ -0,0 +1,22 @@
+#!/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 "$OBJ" || exit 1;
+        $BIN $TOOLARGS \
+                | tee "tools/results/$toolname-$d.txt" "tools/results/last.out"
+        break
+done