static function format_number($number) {
        $formatted = rtrim(format_float($number, 4),'0');
        if (substr($formatted, -1)==get_string('decsep', 'langconfig')) { //if last char is the decimal point
            $formatted .= '0';
        }
        return $formatted;
    }