From d9cb205cef8cc043c6ce43169fb85611c149cd4a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Dec 2007 22:08:45 +0000 Subject: [PATCH] Repeated errors are not duplicated. --- helm/software/matita/bench_disamberrors | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/bench_disamberrors b/helm/software/matita/bench_disamberrors index aaad052c7..87ece78ee 100755 --- a/helm/software/matita/bench_disamberrors +++ b/helm/software/matita/bench_disamberrors @@ -69,12 +69,16 @@ for ma in $sorted_ma_s ; do # this is an error location line if echo "$e" | grep -q "Spurious" ; then loc=$(echo "$e" | sed 's/:.*$//' | cut -f 4 -d ' ') - if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi - spurious_errors="$spurious_errors$loc" + if ! echo "$spurious_errors" | grep -q "$loc"; then + if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi + spurious_errors="$spurious_errors$loc" + fi else loc=$(echo "$e" | sed 's/:.*$//' | cut -f 3 -d ' ') - if ! [ -z "$errors" ] ; then errors="$errors," ; fi - errors="$errors$loc" + if ! echo "$errors" | grep -q "$loc"; then + if ! [ -z "$errors" ] ; then errors="$errors," ; fi + errors="$errors$loc" + fi fi fi error_pass=$(echo "$e" | grep "during phases " | sed 's/:.*$//' | cut -f 6 -d' ' | grep "4\|6") -- 2.39.2