diff options
Diffstat (limited to 'tools/tool.sh')
| -rwxr-xr-x | tools/tool.sh | 29 |
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 | |||
| 8 | CC="$CC -D_POSIX_C_SOURCE=199309L" # For timer | 8 | CC="$CC -D_POSIX_C_SOURCE=199309L" # For timer |
| 9 | 9 | ||
| 10 | BIN="tools/run" | 10 | BIN="tools/run" |
| 11 | d="$(date +'%Y-%m-%d-%H-%M-%S')" | 11 | RESULTS="tools/results" |
| 12 | LAST="$RESULTS/last.out" | ||
| 13 | date="$(date +'%Y-%m-%d-%H-%M-%S')" | ||
| 12 | 14 | ||
| 13 | for t in tools/*; do | 15 | for t in tools/*; do |
| 14 | if [ ! -d "$t" ] || ! (echo "$t" | grep -q "$TOOL"); then | 16 | if [ ! -d "$t" ] || ! (echo "$t" | grep -q "$TOOL"); then |
| 15 | continue | 17 | continue |
| 16 | fi | 18 | fi |
| 17 | toolname="$(basename "$t" .c)" | 19 | toolname="$(basename "$t" .c)" |
| 18 | $CC -o $BIN "$t"/*.c "$OBJ" || exit 1; | ||
| 19 | $BIN $TOOLARGS \ | ||
| 20 | | tee "tools/results/$toolname-$d.txt" "tools/results/last.out" | ||
| 21 | break | 20 | break |
| 22 | done | 21 | done |
| 22 | |||
| 23 | file="$RESULTS/$toolname-$date.txt" | ||
| 24 | |||
| 25 | $CC -o $BIN "$t"/*.c "$OBJ" || exit 1; | ||
| 26 | |||
| 27 | ( | ||
| 28 | date +'%Y-%m-%d %H:%M' | ||
| 29 | echo "" | ||
| 30 | echo "======== config.mk ========" | ||
| 31 | cat config.mk | ||
| 32 | echo "===========================" | ||
| 33 | echo "" | ||
| 34 | echo "=== tool configuration ====" | ||
| 35 | echo "TOOL=$toolname" | ||
| 36 | echo "TOOLARGS=$TOOLARGS" | ||
| 37 | echo "CC=$CC" | ||
| 38 | echo "===========================" | ||
| 39 | echo "" | ||
| 40 | echo "======= tool output =======" | ||
| 41 | $BIN $TOOLARGS | ||
| 42 | echo "===========================" | ||
| 43 | ) | tee "$file" "$LAST" | ||
