1 // “External” variables
2 @font-size-system-ui: 16; // Assumed browser default of `16px`
3 @font-size-vector: 0.875em; // equals `14px` at browser default of `16px`
6 // Colors not on WikimediaUI color palette
7 @background-color-rcfilters-light-gray: #dee0e3;
8 @background-color-rcfilters-light-green: #ccdecc;
10 // Highlight color definitions
11 @highlight-none: #fff;
13 @highlight-c2: #00af89;
15 @highlight-c4: #ff6d22;
16 @highlight-c5: #d73333;
17 @highlight-bluedot: #1d4aad; // Simulates the 'known' browser <li> blue dot
18 @highlight-grey: #54595d; // The color of full dots on Watchlist when highlight is enabled
21 @min-size-circle: 20px;
22 @size-circle: (20 / @font-size-system-ui / @font-size-vector);
23 @margin-circle: (5 / @font-size-system-ui / @font-size-vector);
25 // Result list circle indicators
26 // Defined and used in mw.rcfilters.ui.ChangesListWrapperWidget.less
27 @margin-circle-result: 3px;
28 // In these small sizes, 'em' appears
29 // squished and inconsistent.
30 // Pixels are better for this use case:
31 @size-circle-result: 6px;
33 // Color picker circles
34 @min-size-circle-colorpicker: 30px;
35 @size-circle-colorpicker: (30 / @font-size-system-ui / @font-size-vector);