X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fscripts%2Fpublic_html%2Fshowquery.php;h=dfa0b473068144d1e12e90c6718e45822b7a3d60;hb=6bd0d331d096d862754b42f9a7fb8af1b823685d;hp=1d19033ed7d73275d43ee1513506161829437317;hpb=01dc671e722e9147ae5b3518b0ebcbf86908fd47;p=helm.git diff --git a/helm/software/matita/scripts/public_html/showquery.php b/helm/software/matita/scripts/public_html/showquery.php index 1d19033ed..dfa0b4730 100644 --- a/helm/software/matita/scripts/public_html/showquery.php +++ b/helm/software/matita/scripts/public_html/showquery.php @@ -7,46 +7,13 @@ $qs = array(); foreach($nqs as $v){ $x = explode("@@@",$v); - $qs[$x[0]] = $x[1]; + if ($x[1] == NULL) { + $qs["Unnamed"] = $x[0]; + } else { + $qs[$x[0]] = $x[1]; + } } -function prettify($s,$name) { - if (preg_match("/^[0-9]{12}$/",$s)) { - $year = substr($s,0,4); - $month = substr($s,4,2); - $day = substr($s,6,2); - $hour = substr($s,8,2); - $minute = substr($s,10,2); - return $day . "/" . $month . "/" . $year . " " . $hour . ":" . $minute; - } else if ($name == "sum_time" || $name == "sum_timeuser" || $name == "time" || $name == "time_user" || $name == "timeuser"){ - $min = floor($s / 6000); - $sec = floor(($s - $min * 6000) / 100); - $cents = $s % 100; - return $min . "m" . $sec . "." . $cents . "s"; - } else - return $s; -} - -function printer($q){ - global $i; - echo "
- print $q; ?> + echo $q; ?>