mediawiki.ui variables still contain deprecated color vars. They got deprecated in Iaef72470c59665682f as part of v1.30.
CodeSearch doesn't show results for any of those any more, [[ https://codesearch.wmflabs.org/search/?q=%40colorGray13&i=nope&files=&repos= | exemplified @colorGray13 ]].
Let's remove them.