From cc72a78df3ef850cb09680ae0d9f90aa4cc91861 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Dec 2018 11:43:56 +0100
Subject: Do not exclude "opened" bugs from report

---
 test-suite/report.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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"/
-- 
cgit v1.2.3