fix

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index 42e004f9e7aa56e2bfc80924f6648930d7f70286..0319849267f465abad4718ea2a6cd9522e9ab90b 100644 (file)
--- a/helm/matita/scripts/public_html/bench.php
+++ b/helm/matita/scripts/public_html/bench.php
@@ -46,7 +46,7 @@ $query_total = urlencode("Number of compiled tests@@@select mark, COUNT(DISTINCT
 );
 
 function minus1_to_all($s){
-  if ($s = "-1") 
+  if ($s == "-1") 
     return "all";
   else 
     return $s;