diff options
| author | Gaëtan Gilbert | 2019-02-11 17:05:25 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-11 17:05:25 +0100 |
| commit | d020fbbb2d6d26d1c0c587b2eeee1be3f9f47f49 (patch) | |
| tree | 2f8de938d6b317418d75bb09a327c44b13db3660 | |
| parent | 9352347ee0ea77e0095145afe8c4824a4d5ca32c (diff) | |
Don't save expected failure logs from opened/ bugs.
Grepping for "Error!" is how we decide if we exit with failure or not.
I don't remember why I used the "==> FAILURE <==" string in the
save-logs script but it was an error.
| -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"/ |