From 65878aa07452b45c3f17c3ab15508400edd46476 Mon Sep 17 00:00:00 2001
From: Sebastiano Tronto <sebastiano@tronto.net>
Date: Wed, 18 Sep 2024 07:56:39 +0200
Subject: Some shellcheck

---
 tools/run_tool.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/run_tool.sh b/tools/run_tool.sh
index cec7630..7e09684 100755
--- a/tools/run_tool.sh
+++ b/tools/run_tool.sh
@@ -11,14 +11,14 @@ BIN="tools/run"
 d="$(date +'%Y-%m-%d-%H-%M-%S')"
 
 for t in tools/*; do
-	if [ ! -d "$t" ] || [ -z "$(echo "$t" | grep "$TOOL")" ]; then
+	if [ ! -d "$t" ] || ! (echo "$t" | grep -q "$TOOL"); then
 		continue
 	fi
 	toolname="$(basename "$t" .c)"
-	$CC -o $BIN $t/*.c $CUBEOBJ || exit 1;
+	$CC -o $BIN "$t"/*.c "$CUBEOBJ" || exit 1;
 	$BIN | 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
+rm -rf "$CUBEOBJ"
-- 
cgit v1.3