diff options
Diffstat (limited to 'build_tools')
| -rwxr-xr-x | build_tools/build_documentation.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/build_tools/build_documentation.sh b/build_tools/build_documentation.sh index 232f3469..42b71eac 100755 --- a/build_tools/build_documentation.sh +++ b/build_tools/build_documentation.sh @@ -84,7 +84,7 @@ fi # Destroy TMPLOC echo "Cleaning up '$TMPLOC'" -#rm -Rf "$TMPLOC" +rm -Rf "$TMPLOC" if test $RESULT == 0; then # Tell the user what we did |