# HG changeset patch
# User wenzelm
# Date 1457538039 -3600
# Node ID f4c96158a3b8f21dae14a743282ab3c2f306d3b6
# Parent  5db10482f4cfb45d1188f0fab9831977105fc43c
prefer explicit locale;

diff -r 5db10482f4cf -r f4c96158a3b8 src/Pure/GUI/color_value.scala
--- 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 =