From 18c6848695fbfa97508e0981f6875a6459429a58 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Dec 2005 15:19:50 +0000 Subject: [PATCH] fix --- helm/matita/scripts/public_html/bench.php | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php index 0a09d40ab..bdc238ca5 100644 --- a/helm/matita/scripts/public_html/bench.php +++ b/helm/matita/scripts/public_html/bench.php @@ -46,7 +46,10 @@ $query_total = urlencode("Number of compiled tests@@@select mark, COUNT(DISTINCT ); function minus1_to_all($s){ - if ($s = "-1") return "all" else return $s; + if ($s = "-1") + return "all"; + else + return $s; } function links_of($name,$q){ -- 2.39.2