-
Benedikt Kleinmeier authored
Fix #160: In "TikzGenerator.java", use "String.format(Locale.US, ..." to force a dot as decimal separator.
b36062b1
Fix #160: In "TikzGenerator.java", use "String.format(Locale.US, ..." to force a dot as decimal separator.