fix

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index e0ebe0310efcfd6d807d23a91881d232da315fb6..e2c4db672ad6bed464c79d1b62c26bb5f840f33d 100644 (file)
--- a/helm/matita/scripts/public_html/bench.php
+++ b/helm/matita/scripts/public_html/bench.php
@@ -58,7 +58,7 @@ $query_total = urlencode("Number of compiled tests@@@select mark, COUNT(DISTINCT
       <li><a href="showquery.php?query=<? echo $query_auto; ?>">Auto performances</a></li>
       <li><a href="showquery.php?query=<? echo $query_csc; ?>">Global performances (bytecode)</a></li>
       <li><a href="showquery.php?query=<? echo $query_csc_opt; ?>">Global performances (nativecode)</a></li>
-      <li><a href="showquery.php?query=<? echo $quey_total; ?>">Number of compiled tests</a></li>
+      <li><a href="showquery.php?query=<? echo $query_total; ?>">Number of compiled tests</a></li>
       <li><a href="showquery.php?query=<? echo $quey_all; ?>">All table contents</a></li>
       </ul>
     </p>