--- a/src/Pure/GUI/color_value.scala Wed Mar 09 14:54:51 2016 +0100
+++ b/src/Pure/GUI/color_value.scala Wed Mar 09 16:40:39 2016 +0100
@@ -9,6 +9,7 @@
import java.awt.Color
+import java.util.Locale
object Color_Value
@@ -31,7 +32,7 @@
val g = new java.lang.Integer(c.getGreen)
val b = new java.lang.Integer(c.getBlue)
val a = new java.lang.Integer(c.getAlpha)
- Word.uppercase(String.format("%02x%02x%02x%02x", r, g, b, a))
+ Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a))
}
def apply(s: String): Color =