diff options
Diffstat (limited to 'test-suite/save-logs.sh')
-rwxr-xr-x | test-suite/save-logs.sh | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh deleted file mode 100755 index 9b8fff09..00000000 --- a/test-suite/save-logs.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -SAVEDIR="logs" - -# reset for local builds -rm -rf "$SAVEDIR" -mkdir "$SAVEDIR" - -# keep this synced with test-suite/Makefile -FAILMARK="==========> FAILURE <==========" - -FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" - -rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" -cp summary.log "$SAVEDIR"/ - -# cleanup -rm "$FAILED" |