Only benches with the same result are compared for timing.

diff --git a/matita/scripts/public_html/bench.php b/matita/scripts/public_html/bench.php
index aabc1a50151fd41e24c0cd4558e11c0577721077..eeb3f237b080d7f2da5157caa849371764750956 100644 (file)
--- a/matita/scripts/public_html/bench.php
+++ b/matita/scripts/public_html/bench.php
@@ -44,6 +44,7 @@ where
   b1.test = b2.test and 
   b1.options = b2.options and
   b1.compilation = b2.compilation and 
+  b1.result = b2.result and 
   b1.mark = '$before_last_mark' and b2.mark= '$last_mark' and
   ABS(b2.timeuser - b1.timeuser) > 100
 order by diff desc***");
@@ -355,6 +356,7 @@ where
   b1.test = b2.test and 
   b1.options = b2.options and
   b1.compilation = b2.compilation and 
+  b1.result = b2.result and 
   b1.mark = '<?php echo $before_last_mark ?>' and b2.mark= '<?php echo $last_mark ?>' and
   ABS(b2.timeuser - b1.timeuser) &lt; 100
 order by diff desc;