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

---
 helm/matita/scripts/public_html/bench.php | 2 +-
 helm/matita/scripts/public_html/style.css | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 helm/matita/scripts/public_html/style.css

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index 366b8dcb0..31596cc64 100644
--- a/helm/matita/scripts/public_html/bench.php
+++ b/helm/matita/scripts/public_html/bench.php
@@ -57,7 +57,7 @@ function minus1_to_all($s){
 function links_of($name,$q,$limits){
   echo "<li>$name :&nbsp;&nbsp;&nbsp;";
   if (strpos($q, urlencode("***")) === false) {
-    echo "<a href=\"showquery.php?query=$q1;\">all</a>";
+    echo "<a href=\"showquery.php?query=$q;\">all</a>";
   } else {
     foreach($limits as $l) {
       $q1 = str_replace(urlencode("***"), " LIMIT 0,$l", $q);
diff --git a/helm/matita/scripts/public_html/style.css b/helm/matita/scripts/public_html/style.css
new file mode 100644
index 000000000..498db558e
--- /dev/null
+++ b/helm/matita/scripts/public_html/style.css
@@ -0,0 +1,8 @@
+body {
+  font-family: sans-serif;
+  font-size: 12pt;
+}
+
+a {
+  border: blue 1pt;
+}
-- 
2.39.2