From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2007 22:08:45 +0000 (+0000)
Subject: Repeated errors are not duplicated.
X-Git-Tag: make_still_working~5727
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9cb205cef8cc043c6ce43169fb85611c149cd4a;p=helm.git

Repeated errors are not duplicated.
---

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")