Clean up tool output

1 files changed, 25 insertions, 4 deletions

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"