diff options
| author | Maxime Dénès | 2019-02-13 21:57:34 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-13 21:57:34 +0100 |
| commit | 0e36b06e8426d2fcd18fafed187a676ceb6592ae (patch) | |
| tree | ce1d742e51225febb8344d15edb41a324f7d763b | |
| parent | 64eaf184df8ca52b7254a03e3b4f87c3c0491fdd (diff) | |
| parent | d020fbbb2d6d26d1c0c587b2eeee1be3f9f47f49 (diff) | |
Merge PR #9554: Don't save expected failure logs from opened/ bugs.
Reviewed-by: maximedenes
| -rwxr-xr-x | test-suite/report.sh | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/test-suite/report.sh b/test-suite/report.sh index 71aac029ea..5b74bee0c7 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -11,11 +11,8 @@ SAVEDIR="logs" rm -rf "$SAVEDIR" mkdir "$SAVEDIR" -# keep this synced with test-suite/Makefile -FAILMARK="==========> FAILURE <==========" - FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" +find . '(' -name '*.log' -exec grep -q -F "Error!" '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" cp summary.log "$SAVEDIR"/ |