Browse Source

Delete temporary files from warning filtering

Steven Engler 4 years ago
parent
commit
17cae1a348
1 changed files with 1 additions and 0 deletions
  1. 1 0
      tools/warnings.sh

+ 1 - 0
tools/warnings.sh

@@ -77,6 +77,7 @@ show_warnings() {
     if [ "$CHUTNEY_WARNINGS_SUMMARY" != true ]; then
     if [ "$CHUTNEY_WARNINGS_SUMMARY" != true ]; then
         $ECHO_Q ""
         $ECHO_Q ""
     fi
     fi
+    rm "${LOGS}" "${FILTERED_LOGS}"
 }
 }
 
 
 usage() {
 usage() {