From d020fbbb2d6d26d1c0c587b2eeee1be3f9f47f49 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Feb 2019 17:05:25 +0100
Subject: 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.
---
 test-suite/report.sh | 5 +----
 1 file changed, 1 insertion(+), 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"/
-- 
cgit v1.2.3