diff options
Diffstat (limited to 'tools/run_tool.sh')
| -rwxr-xr-x | tools/run_tool.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/run_tool.sh b/tools/run_tool.sh index 2462b2d..cec7630 100755 --- a/tools/run_tool.sh +++ b/tools/run_tool.sh | |||
| @@ -16,7 +16,7 @@ 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" | 19 | $BIN | tee "tools/results/$toolname-$d.txt" "tools/results/last.out" |
| 20 | break | 20 | break |
| 21 | done | 21 | done |
| 22 | 22 | ||
