Cast added due to API changes in PHP 5.3.1

diff --git a/inc/functions.php b/inc/functions.php
index 69477a7dc847bc199728c6894e5948d69559cee1..b21b98e90a754a042def35c4ba88311c7c1348e9 100644 (file)
--- a/inc/functions.php
+++ b/inc/functions.php
@@ -785,6 +785,9 @@ function translatePoolType ($type) {
 
 // Translates the american decimal dot into a german comma
 function translateComma ($dotted, $cut = true, $max = '0') {
+       // First, cast all to double, due to PHP changes
+       $dotted = (double) $dotted;
+
        // Default is 3 you can change this in admin area "Misc -> Misc Options"
        if (!isConfigEntrySet('max_comma')) setConfigEntry('max_comma', 3);