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/run_tool.sh | 25 -------------------------
 1 file changed, 25 deletions(-)
 delete mode 100755 tools/run_tool.sh

(limited to 'tools/run_tool.sh')

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