src/Pure/GUI/color_value.scala
changeset 70083 96776eb41854
parent 64370 865b39487b5d
child 71381 b9ea2467c929
equal deleted inserted replaced
70082:4f936de6d9b8 70083:96776eb41854
    43           cache += (s -> c)
    43           cache += (s -> c)
    44           c
    44           c
    45       }
    45       }
    46     }
    46     }
    47 }
    47 }
    48