diff options
Diffstat (limited to 'tools/run_tool.sh')
| -rwxr-xr-x | tools/run_tool.sh | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/run_tool.sh b/tools/run_tool.sh index 7e09684..2216a66 100755 --- a/tools/run_tool.sh +++ b/tools/run_tool.sh | |||
| @@ -5,7 +5,7 @@ if [ -z "$TOOL" ]; then | |||
| 5 | exit 1 | 5 | exit 1 |
| 6 | fi | 6 | fi |
| 7 | 7 | ||
| 8 | CC="$CC -D_POSIX_C_SOURCE=199309L" | 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 | d="$(date +'%Y-%m-%d-%H-%M-%S')" |
| @@ -16,7 +16,8 @@ for t in tools/*; do | |||
| 16 | fi | 16 | fi |
| 17 | toolname="$(basename "$t" .c)" | 17 | toolname="$(basename "$t" .c)" |
| 18 | $CC -o $BIN "$t"/*.c "$CUBEOBJ" || exit 1; | 18 | $CC -o $BIN "$t"/*.c "$CUBEOBJ" || exit 1; |
| 19 | $BIN | tee "tools/results/$toolname-$d.txt" "tools/results/last.out" | 19 | $BIN $TOOLARGS \ |
| 20 | | tee "tools/results/$toolname-$d.txt" "tools/results/last.out" | ||
| 20 | break | 21 | break |
| 21 | done | 22 | done |
| 22 | 23 | ||
