From c8e76fcb951b09075cc9104cc2046462f757dd61 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 22 Dec 2005 09:56:14 +0000
Subject: [PATCH] fix

---
 helm/matita/scripts/public_html/bench.php | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index c1c241354..366b8dcb0 100644
--- 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>";
 }
 
-- 
2.39.2