fix

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index 0a09d40abe27be706fec73c03e67cb295462ddc7..bdc238ca5f026f9e47b1f1c501c79e71493040a4 100644 (file)
--- a/helm/matita/scripts/public_html/bench.php
+++ b/helm/matita/scripts/public_html/bench.php
@@ -46,7 +46,10 @@ $query_total = urlencode("Number of compiled tests@@@select mark, COUNT(DISTINCT
 );
 
 function minus1_to_all($s){
-  if ($s = "-1") return "all" else return $s;
+  if ($s = "-1") 
+    return "all";
+  else 
+    return $s;
 }
 
 function links_of($name,$q){