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 -------------------------
 tools/tool.sh     | 22 ++++++++++++++++++++++
 2 files changed, 22 insertions(+), 25 deletions(-)
 delete mode 100755 tools/run_tool.sh
 create mode 100755 tools/tool.sh

(limited to 'tools')

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"
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