Bug fixed: \n prevented recognition.

diff --git a/helm/software/matita/bench_summary.py b/helm/software/matita/bench_summary.py
index cbf877bfe4b3d56ebea8a3db685d5217c318ea90..64f3ad39dd4123a21cf63956efe832849ecdaae3 100755 (executable)
--- a/helm/software/matita/bench_summary.py
+++ b/helm/software/matita/bench_summary.py
@@ -11,6 +11,7 @@ stats['mistakes'] = []
 stats['undetected'] = []
 
 for line in open(sys.argv[1]):
 stats['undetected'] = []
 
 for line in open(sys.argv[1]):

+    line = line.rstrip()

     if line[0] == '#':
         continue
     cols = line.split('|')
     if line[0] == '#':
         continue
     cols = line.split('|')


@@ -69,7 +70,7 @@ print format_stat('undetected')
 print r'\hline'
 print format_stat('total')
 print r'\\'
 print r'\hline'
 print format_stat('total')
 print r'\\'

-print r'%-15s & %6.1f & \\' % ('spurious avg',
+print r'%-15s & %6.1f & \\' % ('spurious average',

         float(stats['spurious']['tot']) / len(stats['precise']))
 print r'%-15s & %6d & \\' % ('spurious max',
         float(stats['spurious']['max']))
         float(stats['spurious']['tot']) / len(stats['precise']))
 print r'%-15s & %6d & \\' % ('spurious max',
         float(stats['spurious']['max']))