diff options
| author | Gaëtan Gilbert | 2018-12-21 13:58:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-21 13:58:13 +0100 |
| commit | ee98d818791d8f92674934cda02bfcb3667013c9 (patch) | |
| tree | da45b9df79f73485c690dedcd7213c20444478df | |
| parent | d501e6f301f1c023e57f14ee3441553c530d9394 (diff) | |
| parent | cc72a78df3ef850cb09680ae0d9f90aa4cc91861 (diff) | |
Merge PR #9265: Do not exclude "opened" bugs from report
| -rwxr-xr-x | test-suite/report.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/report.sh b/test-suite/report.sh index c5e698232f..cef615266b 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -15,7 +15,7 @@ mkdir "$SAVEDIR" FAILMARK="==========> FAILURE <==========" FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" +find . '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" cp summary.log "$SAVEDIR"/ |