fix

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index c1c241354d0bfc96bd649691a3c8d4477a358f27..366b8dcb09aa341c12fcfb31a869f7207b33c21a 100644 (file)
--- a/helm/matita/scripts/public_html/bench.php
+++ b/helm/matita/scripts/public_html/bench.php
@@ -56,15 +56,18 @@ function minus1_to_all($s){
 
 function links_of($name,$q,$limits){
   echo "<li>$name :&nbsp;&nbsp;&nbsp;";
-  foreach($limits as $l) {
-    $q1 = str_replace(urlencode("***"), " LIMIT 0,$l", $q);
-    echo "<a href=\"showquery.php?query=$q1;\">" . 
-          minus1_to_all($l) . "</a>&nbsp;&nbsp;";
+  if (strpos($q, urlencode("***")) === false) {
+    echo "<a href=\"showquery.php?query=$q1;\">all</a>";
+  } else {
+    foreach($limits as $l) {
+      $q1 = str_replace(urlencode("***"), " LIMIT 0,$l", $q);
+      echo "<a href=\"showquery.php?query=$q1;\">" . 
+            minus1_to_all($l) . "</a>&nbsp;&nbsp;";
+    }
+      $q1 = str_replace(urlencode("***"), " LIMIT 0,-1", $q);
+      echo "<a href=\"showquery.php?query=$q1;\">" . 
+            minus1_to_all("-1") . "</a>&nbsp;&nbsp;";
   }
-    $q1 = str_replace(urlencode("***"), " LIMIT 0,-1", $q);
-    echo "<a href=\"showquery.php?query=$q1;\">" . 
-          minus1_to_all("-1") . "</a>&nbsp;&nbsp;";
-  
   echo "</li>";
 }