RCFilters UI: Use pixel instead of em for distancing the highlight dots

Also, make the circles slightly bigger; the 5px value made the circles
look slightly squarish, so we increase the radius by 1 pixel to 6px.

Bug: T161258
Change-Id: I483dc698ba15380990ded097caec24b408fba43a

diff --git a/resources/src/mediawiki.rcfilters/styles/mw.rcfilters.variables.less b/resources/src/mediawiki.rcfilters/styles/mw.rcfilters.variables.less
index 1ef49e2..3060f25 100644 (file)
--- a/resources/src/mediawiki.rcfilters/styles/mw.rcfilters.variables.less
+++ b/resources/src/mediawiki.rcfilters/styles/mw.rcfilters.variables.less
@@ -11,9 +11,9 @@
 
 // Result list circle indicators
 // Defined and used in mw.rcfilters.ui.ChangesListWrapperWidget.less
-@result-circle-margin: 0.1em;
+@result-circle-margin: 3px;
 @result-circle-general-margin: 0.5em;
 // In these small sizes, 'em' appears
 // squished and inconsistent.
 // Pixels are better for this use case:
-@result-circle-diameter: 5px;
+@result-circle-diameter: 6px;