From b8d17736ce2c85174a47c7200ef6d19a51d0c347 Mon Sep 17 00:00:00 2001
From: Sebastiano Tronto <sebastiano@tronto.net>
Date: Wed, 2 Oct 2024 18:37:36 +0200
Subject: Do not run make clean automatically on every build and other Makefile
 changes

---
 tools/tool.sh | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100755 tools/tool.sh

(limited to 'tools/tool.sh')

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
-- 
cgit v1.3