Repeated errors are not duplicated.

diff --git a/helm/software/matita/bench_disamberrors b/helm/software/matita/bench_disamberrors
index aaad052c7924b5c66b5d0b7147f47bcc853e9e88..87ece78eec4606f14bf59bd1108eaa7195a0a1f8 100755 (executable)
--- 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")