From 32009294d2de3e197c8d4dc950559ff948ea2fc9 Mon Sep 17 00:00:00 2001
From: Sebastiano Tronto <sebastiano@tronto.net>
Date: Fri, 4 Oct 2024 08:58:47 +0200
Subject: Clean up tool output

---
 tools/tool.sh | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

(limited to 'tools/tool.sh')

diff --git a/tools/tool.sh b/tools/tool.sh
index 64bfd89..23d781d 100755
--- a/tools/tool.sh
+++ b/tools/tool.sh
@@ -8,15 +8,36 @@ fi
 CC="$CC -D_POSIX_C_SOURCE=199309L" # For timer
 
 BIN="tools/run"
-d="$(date +'%Y-%m-%d-%H-%M-%S')"
+RESULTS="tools/results"
+LAST="$RESULTS/last.out"
+date="$(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
+
+file="$RESULTS/$toolname-$date.txt"
+
+$CC -o $BIN "$t"/*.c "$OBJ" || exit 1;
+
+(
+date +'%Y-%m-%d %H:%M'
+echo ""
+echo "======== config.mk ========"
+cat config.mk
+echo "==========================="
+echo ""
+echo "=== tool configuration ===="
+echo "TOOL=$toolname"
+echo "TOOLARGS=$TOOLARGS"
+echo "CC=$CC"
+echo "==========================="
+echo ""
+echo "======= tool output ======="
+$BIN $TOOLARGS 
+echo "==========================="
+) | tee "$file" "$LAST"
-- 
cgit v1.3