Question for those who use comma as decimal separator

Not the official traditional separator. Have you heard of the Academies of the Language? French has one; Spanish has 22 but they publish a single Ortografía.

I think it is worth at least beta-testing your idea of displaying coordinates as X 12.34 Y 56.78 (or RA/Dec or whatever the coordinates are called in the game). Instantly legible no matter how the operating system displays decimal fractions, and no extra parentheses or vertical lines cluttering up the display.

It’s ###.# instead of ##.##, but same difference.

The issue with “X 123.4 Y 567.8” is the extra horizontal space that uses up compared to “(123.4|567.8)”. It’s not a ton, but enough to matter.

Yes, I do know about language academies and other regulatory bodies. For example, here is Quebec’s Office of the French language suggesting the use of a comma as decimal separator (in units of measurement, but it’s similar for numbers in general).

I’m not exactly sure what you’re saying: is it that the upper comma was a commonly used decimal separator but never officially, or that regulatory bodies in Spain and France were (or are) in fact suggesting using the upper comma?

That the high comma was and remains still the official sign in Spanish when possible (a lot of Spanish orthographic rules apply “when possible”, to avoid driving people nuts over something which the medium simply doesn’t allow for); other separators are now accepted where previously they would have been not, again due to limited possibilities. I don’t know whether the Académie listed that detail officially or not, but I do know it is what my older French coworkers grew up with and what older Italian people still use… when possible.