They became deprecated in Iaef72470c59665. It's time to remove them.
Bug: T210118
Change-Id: Ibc761a2cdc8d04213d149851129cd51ee4661899
// Form input sizes, equal to OOUI at 14px base font-size
@sizeInputBinary: 1.5625em;
-
-// Deprecated color variables from when WikimediaUI color palette wasn't around
-// See https://wikimedia.github.io/WikimediaUI-Style-Guide/visual-style_colors.html
-@colorGray3: #333;
-@colorGray6: #666;
-@colorGray8: #888;
-@colorGray9: #999;
-@colorGray11: #bbb;
-@colorGray13: #ddd;