diff options
Diffstat (limited to 'tools/run_tool.sh')
| -rwxr-xr-x | tools/run_tool.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/run_tool.sh b/tools/run_tool.sh index 495d68c..2462b2d 100755 --- a/tools/run_tool.sh +++ b/tools/run_tool.sh | |||
| @@ -20,4 +20,5 @@ for t in tools/*; do | |||
| 20 | break | 20 | break |
| 21 | done | 21 | done |
| 22 | 22 | ||
| 23 | rm -rf $BIN $CUBEOBJ | 23 | # $BIN is kept so it can be run manually for profiling |
| 24 | rm -rf $CUBEOBJ | ||
