diff options
Diffstat (limited to 'test-suite/save-logs.sh')
-rwxr-xr-x | test-suite/save-logs.sh | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh new file mode 100755 index 00000000..9b8fff09 --- /dev/null +++ b/test-suite/save-logs.sh @@ -0,0 +1,19 @@ +#!/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" |