diff options
| author | Maxime Dénès | 2018-12-21 11:43:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-21 11:45:26 +0100 |
| commit | cc72a78df3ef850cb09680ae0d9f90aa4cc91861 (patch) | |
| tree | ef52a41c8a05b9224f23656bb81bc290213d0a73 | |
| parent | ba6b5839add7587837b4cea890f2d505ce76d489 (diff) | |
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"/ |