fix

diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php
index 95243617ce97eb68504330e956fd7bab6486b633..07b468cc83c9b68964fddc353e478897dd967baf 100644 (file)
--- a/helm/matita/scripts/public_html/bench.php
+++ b/helm/matita/scripts/public_html/bench.php
@@ -12,7 +12,7 @@ $query_fail = urlencode(
   "select mark, count(distinct test) as fail_no from bench where result = 'fail' group by mark order by mark desc;"
   . "###" . 
   "Tests failed:@@@" .
-  "select distinct mark, test, result from bench where result = 'fail' sort by mark desc;" 
+  "select distinct mark, test, result from bench where result = 'fail' order by mark desc;" 
 );
 $query_gc = urlencode(
   "GC usage @@@" .