This ensures that we always use . as decimal separator, regardless of the user locale (which might use , or something else). References #713