fix

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index 366b8dcb09aa341c12fcfb31a869f7207b33c21a..31596cc64e7a4c6fc696097a384b65a704d80034 100644 (file)
--- 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 (file)
index 0000000..498db55
--- /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;
+}