-function time_to_decimal($a) {
- $tmp = explode(":", $a);
- if($tmp[1]{0}=="0") $tmp[1] = $tmp[1]{1};
+// time_to_decimal converts a time string such as 1:15 to its decimal representation such as 1.25 or 1,25.
+function time_to_decimal($val) {
+ global $user;
+ $parts = explode(':', $val); // parts[0] is hours, parts[1] is minutes.