-
Benedikt Kleinmeier authored
Fix #160: In "TikzGenerator.java", use "String.format(Locale.US, ..." to force a dot as decimal separator.
b36062b1
29. April 2024: Due to updates GitLab may be unavailable for some minutes between 10:00 and 12:00.
Fix #160: In "TikzGenerator.java", use "String.format(Locale.US, ..." to force a dot as decimal separator.