From 15ccb842eabab6445f4bc626bd38f281c763d993 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 18 Apr 2007 09:10:30 +0000
Subject: [PATCH] Only benches with the same result are compared for timing.

---
 matita/scripts/public_html/bench.php | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/matita/scripts/public_html/bench.php b/matita/scripts/public_html/bench.php
index aabc1a501..eeb3f237b 100644
--- 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;
-- 
2.39.2