MD Settings: implement "controlled by" indicator UI

MD Settings: implement "controlled by" indicator UI

R=michaelpg@chromium.org
BUG=614265
CQ_INCLUDE_TRYBOTS=tryserver.chromium.linux:closure_compilation

Committed: https://crrev.com/a67b4e040e5618f4ff21a64c3c2a813f17af87a4
Cr-Commit-Position: refs/heads/master@{#396588}

[Dan Beam, 2016-05-27 01:58:05]

Description was changed from

==========
MD Settings: implement "controlled by" indicator UI

R=michaelpg@chromium.org
BUG=614265
==========

to

==========
MD Settings: implement "controlled by" indicator UI

R=michaelpg@chromium.org
BUG=614265
CQ_INCLUDE_TRYBOTS=tryserver.chromium.linux:closure_compilation
==========

[Dan Beam, 2016-05-27 02:13:28]

Patchset #1 (id:1) has been deleted

[Dan Beam, 2016-05-27 02:14:52]

whole section on mouse hover: http://i.imgur.com/owaLN2j.png
when focused via Tab: http://i.imgur.com/IfBxMNr.png

[michaelpg, 2016-05-27 19:00:26]

On 2016/05/27 02:14:52, Dan Beam wrote:
> whole section on mouse hover: http://i.imgur.com/owaLN2j.png
> when focused via Tab: http://i.imgur.com/IfBxMNr.png

Huh? Why, and how, is the font different between these two?

[Dan Beam, 2016-05-27 19:28:14]

On 2016/05/27 19:00:26, michaelpg wrote:
> On 2016/05/27 02:14:52, Dan Beam wrote:
> > whole section on mouse hover: http://i.imgur.com/owaLN2j.png
> > when focused via Tab: http://i.imgur.com/IfBxMNr.png
> 
> Huh? Why, and how, is the font different between these two?

because it was before I noticed the spec asks for 12px font instead of 13px, so
the smaller one is the final, fixed, correct font-size

[stevenjb, 2016-05-27 20:45:09]

stevenjb@chromium.org changed reviewers:
+ stevenjb@chromium.org

[stevenjb, 2016-05-27 20:45:10]

lgtm

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
File ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html
(right):

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:13:
font-size: 92.31%;  /* Effectively 12px if the host default is 13px. */
92.31% seems... fragile. Grepping the existing code I see a mix of px, %, and
one use of 'em'.

No need to do this now, but I would advocate for a consistency pass. 

My experience outside of HTML suggests that explicit sets of font sizes work
better than percentages (i.e. 92.31% may not look good if the default changes to
14px or the font changes), which suggests to me that we would be better off
using CSS variables for font sizes. That said, I have very little experience
with font sizes in HTML.

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:14:
font-weight: 500;
We use 'bold' in a few places still, it would be good to make that consistent at
the same time. CSS variables seem like a good idea here too since my
understanding is that not all font weights will be noticeably different on all
fonts (and we currently use 400, 500, and 600).

[Dan Beam, 2016-05-27 21:40:20]

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
File ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html
(right):

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:13:
font-size: 92.31%;  /* Effectively 12px if the host default is 13px. */
On 2016/05/27 20:45:09, stevenjb wrote:
> 92.31% seems... fragile. Grepping the existing code I see a mix of px, %, and
> one use of 'em'.
> 
> No need to do this now, but I would advocate for a consistency pass. 
> 
> My experience outside of HTML suggests that explicit sets of font sizes work
> better than percentages (i.e. 92.31% may not look good if the default changes
to
> 14px or the font changes), which suggests to me that we would be better off
> using CSS variables for font sizes. That said, I have very little experience
> with font sizes in HTML.

em and % are both scalable font-size units.  getting them consistent is not
really a goal of mine.  using an absolute px length here would have functional
issues when the user changes their default "Web Content" font size.

for example: the default font-size in Chrome is 13px.  when that's changed from
settings to 26px, any element with a hardcoded "13px" doesn't adapt and looks
out of place (and may be inaccessible to users with poor vision).

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:14:
font-weight: 500;
On 2016/05/27 20:45:09, stevenjb wrote:
> We use 'bold' in a few places still, it would be good to make that consistent
at
> the same time. CSS variables seem like a good idea here too since my
> understanding is that not all font weights will be noticeably different on all
> fonts (and we currently use 400, 500, and 600).

chrome bundles Roboto with weights of 400, 500, and 700.

they all look different.

400 is "normal" (both in CSS and spec terms)
500 is "medium" (spec)
700 is "bold" (both CSS and spec terms, this weight didn't exist until recently)

there was previously 300 that was called "light" in specs and used in only 1
place (incognito NTP).  it was removed because it was adding size to chrome for
little benefit.

[stevenjb, 2016-05-27 21:54:12]

BTW, I am not trying to be difficult here, I am just genuinely perplexed by the
variety of font sizing practices just within Settings. We absolutely do not need
to hash this out here, I just found the "92.31%" value somewhat striking - it
does not seem especially maintainable.

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
File ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html
(right):

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:13:
font-size: 92.31%;  /* Effectively 12px if the host default is 13px. */
On 2016/05/27 21:40:19, Dan Beam wrote:
> On 2016/05/27 20:45:09, stevenjb wrote:
> > 92.31% seems... fragile. Grepping the existing code I see a mix of px, %,
and
> > one use of 'em'.
> > 
> > No need to do this now, but I would advocate for a consistency pass. 
> > 
> > My experience outside of HTML suggests that explicit sets of font sizes work
> > better than percentages (i.e. 92.31% may not look good if the default
changes
> to
> > 14px or the font changes), which suggests to me that we would be better off
> > using CSS variables for font sizes. That said, I have very little experience
> > with font sizes in HTML.
> 
> em and % are both scalable font-size units.  getting them consistent is not
> really a goal of mine.  using an absolute px length here would have functional
> issues when the user changes their default "Web Content" font size.
> 
> for example: the default font-size in Chrome is 13px.  when that's changed
from
> settings to 26px, any element with a hardcoded "13px" doesn't adapt and looks
> out of place (and may be inaccessible to users with poor vision).

So are you saying we should be using all three (px, %, and em)? As someone only
passingly familiar with font sizing if I look at the existing code it is unclear
what pattern I should follow.

Will 92.31% still look correct if the default font size is changed to, say,
15px? If so, would "90%" work just as well here?

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:14:
font-weight: 500;
On 2016/05/27 21:40:20, Dan Beam wrote:
> On 2016/05/27 20:45:09, stevenjb wrote:
> > We use 'bold' in a few places still, it would be good to make that
consistent
> at
> > the same time. CSS variables seem like a good idea here too since my
> > understanding is that not all font weights will be noticeably different on
all
> > fonts (and we currently use 400, 500, and 600).
> 
> chrome bundles Roboto with weights of 400, 500, and 700.
> 
> they all look different.
> 
> 400 is "normal" (both in CSS and spec terms)
> 500 is "medium" (spec)
> 700 is "bold" (both CSS and spec terms, this weight didn't exist until
recently)

What abut 600, which we currently use in bluetooth_device_dialog.html? 

> 
> there was previously 300 that was called "light" in specs and used in only 1
> place (incognito NTP).  it was removed because it was adding size to chrome
for
> little benefit.

[Dan Beam, 2016-05-27 22:00:49]

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
File ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html
(right):

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:13:
font-size: 92.31%;  /* Effectively 12px if the host default is 13px. */
On 2016/05/27 21:54:12, stevenjb wrote:
> On 2016/05/27 21:40:19, Dan Beam wrote:
> > On 2016/05/27 20:45:09, stevenjb wrote:
> > > 92.31% seems... fragile. Grepping the existing code I see a mix of px, %,
> and
> > > one use of 'em'.
> > > 
> > > No need to do this now, but I would advocate for a consistency pass. 
> > > 
> > > My experience outside of HTML suggests that explicit sets of font sizes
work
> > > better than percentages (i.e. 92.31% may not look good if the default
> changes
> > to
> > > 14px or the font changes), which suggests to me that we would be better
off
> > > using CSS variables for font sizes. That said, I have very little
experience
> > > with font sizes in HTML.
> > 
> > em and % are both scalable font-size units.  getting them consistent is not
> > really a goal of mine.  using an absolute px length here would have
functional
> > issues when the user changes their default "Web Content" font size.
> > 
> > for example: the default font-size in Chrome is 13px.  when that's changed
> from
> > settings to 26px, any element with a hardcoded "13px" doesn't adapt and
looks
> > out of place (and may be inaccessible to users with poor vision).
> 
> So are you saying we should be using all three (px, %, and em)?

no, we attempt to never use px when the font-size may vary.  either % or em are
acceptable.

> As someone only
> passingly familiar with font sizing if I look at the existing code it is
unclear
> what pattern I should follow.

the nearby convention.

> 
> Will 92.31% still look correct if the default font size is changed to, say,
> 15px? If so, would "90%" work just as well here?

if the user changes their default font size from 13px to 15px, I would expect
tooltips' font to also change proportionally.  are you asking, "will 92.31% x 15
be a round number?" no, not necesarilly, but I don't think that's an expectation
or really matters much.

https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:14:
font-weight: 500;
On 2016/05/27 21:54:12, stevenjb wrote:
> On 2016/05/27 21:40:20, Dan Beam wrote:
> > On 2016/05/27 20:45:09, stevenjb wrote:
> > > We use 'bold' in a few places still, it would be good to make that
> consistent
> > at
> > > the same time. CSS variables seem like a good idea here too since my
> > > understanding is that not all font weights will be noticeably different on
> all
> > > fonts (and we currently use 400, 500, and 600).
> > 
> > chrome bundles Roboto with weights of 400, 500, and 700.
> > 
> > they all look different.
> > 
> > 400 is "normal" (both in CSS and spec terms)
> > 500 is "medium" (spec)
> > 700 is "bold" (both CSS and spec terms, this weight didn't exist until
> recently)
> 
> What abut 600, which we currently use in bluetooth_device_dialog.html? 
> 
> > 
> > there was previously 300 that was called "light" in specs and used in only 1
> > place (incognito NTP).  it was removed because it was adding size to chrome
> for
> > little benefit.
> 

the situation may differ slightly on ChromeOS (I think Roboto is a system font
there?), but in desktop: if you use font-weight: 600; it'd just take some other
weight (i.e. 400) and interpolate the glyphs.  kind of like if you have a small
image and display it at a large size: the browser just takes its best guess at
what it should look like but it generally doesn't look good nor is it defined.

[stevenjb, 2016-05-27 22:38:27]

On 2016/05/27 22:00:49, Dan Beam wrote:
>
https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
> File ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html
> (right):
> 
>
https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
> ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:13:
> font-size: 92.31%;  /* Effectively 12px if the host default is 13px. */
> On 2016/05/27 21:54:12, stevenjb wrote:
> > On 2016/05/27 21:40:19, Dan Beam wrote:
> > > On 2016/05/27 20:45:09, stevenjb wrote:
> > > > 92.31% seems... fragile. Grepping the existing code I see a mix of px,
%,
> > and
> > > > one use of 'em'.
> > > > 
> > > > No need to do this now, but I would advocate for a consistency pass. 
> > > > 
> > > > My experience outside of HTML suggests that explicit sets of font sizes
> work
> > > > better than percentages (i.e. 92.31% may not look good if the default
> > changes
> > > to
> > > > 14px or the font changes), which suggests to me that we would be better
> off
> > > > using CSS variables for font sizes. That said, I have very little
> experience
> > > > with font sizes in HTML.
> > > 
> > > em and % are both scalable font-size units.  getting them consistent is
not
> > > really a goal of mine.  using an absolute px length here would have
> functional
> > > issues when the user changes their default "Web Content" font size.
> > > 
> > > for example: the default font-size in Chrome is 13px.  when that's changed
> > from
> > > settings to 26px, any element with a hardcoded "13px" doesn't adapt and
> looks
> > > out of place (and may be inaccessible to users with poor vision).
> > 
> > So are you saying we should be using all three (px, %, and em)?
> 
> no, we attempt to never use px when the font-size may vary.  either % or em
are
> acceptable.
> 
> > As someone only
> > passingly familiar with font sizing if I look at the existing code it is
> unclear
> > what pattern I should follow.
> 
> the nearby convention.
> 
> > 
> > Will 92.31% still look correct if the default font size is changed to, say,
> > 15px? If so, would "90%" work just as well here?
> 
> if the user changes their default font size from 13px to 15px, I would expect
> tooltips' font to also change proportionally.  are you asking, "will 92.31% x
15
> be a round number?" no, not necesarilly, but I don't think that's an
expectation
> or really matters much.
> 
>
https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
> ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:14:
> font-weight: 500;
> On 2016/05/27 21:54:12, stevenjb wrote:
> > On 2016/05/27 21:40:20, Dan Beam wrote:
> > > On 2016/05/27 20:45:09, stevenjb wrote:
> > > > We use 'bold' in a few places still, it would be good to make that
> > consistent
> > > at
> > > > the same time. CSS variables seem like a good idea here too since my
> > > > understanding is that not all font weights will be noticeably different
on
> > all
> > > > fonts (and we currently use 400, 500, and 600).
> > > 
> > > chrome bundles Roboto with weights of 400, 500, and 700.
> > > 
> > > they all look different.
> > > 
> > > 400 is "normal" (both in CSS and spec terms)
> > > 500 is "medium" (spec)
> > > 700 is "bold" (both CSS and spec terms, this weight didn't exist until
> > recently)
> > 
> > What abut 600, which we currently use in bluetooth_device_dialog.html? 
> > 
> > > 
> > > there was previously 300 that was called "light" in specs and used in only
1
> > > place (incognito NTP).  it was removed because it was adding size to
chrome
> > for
> > > little benefit.
> > 
> 
> the situation may differ slightly on ChromeOS (I think Roboto is a system font
> there?), but in desktop: if you use font-weight: 600; it'd just take some
other
> weight (i.e. 400) and interpolate the glyphs.  kind of like if you have a
small
> image and display it at a large size: the browser just takes its best guess at
> what it should look like but it generally doesn't look good nor is it defined.

I think you misunderstand me. We *are* using 600, probably copied from old
settings, but apparently *shouldn't* be. This is not documented anywhere. I
think that is a problem, and I think we have a similar problem with font sizes.
Using 93.21% everywhere we want "slightly smaller than default" requires an
extra comment just to make it semi readable. If you do not think this is a
problem that is fine, obviously I do not have as much time to focus on any of
this as I would like to, otherwise I would volunteer to help improve it :(

[Dan Beam, 2016-05-27 22:39:13]

The CQ bit was checked by dbeam@chromium.org

[commit-bot: I haz the power, 2016-05-27 22:39:33]

CQ is trying da patch. Follow status at
 https://chromium-cq-status.appspot.com/patch-status/2019563002/20001
View timeline at
 https://chromium-cq-status.appspot.com/patch-timeline/2019563002/20001

[commit-bot: I haz the power, 2016-05-27 22:43:50]

Committed patchset #1 (id:20001)

[commit-bot: I haz the power, 2016-05-27 22:46:07]

Description was changed from

==========
MD Settings: implement "controlled by" indicator UI

R=michaelpg@chromium.org
BUG=614265
CQ_INCLUDE_TRYBOTS=tryserver.chromium.linux:closure_compilation
==========

to

==========
MD Settings: implement "controlled by" indicator UI

R=michaelpg@chromium.org
BUG=614265
CQ_INCLUDE_TRYBOTS=tryserver.chromium.linux:closure_compilation

Committed: https://crrev.com/a67b4e040e5618f4ff21a64c3c2a813f17af87a4
Cr-Commit-Position: refs/heads/master@{#396588}
==========

[commit-bot: I haz the power, 2016-05-27 22:46:08]

Patchset 1 (id:??) landed as
https://crrev.com/a67b4e040e5618f4ff21a64c3c2a813f17af87a4
Cr-Commit-Position: refs/heads/master@{#396588}

[Dan Beam, 2016-05-27 22:56:18]

On 2016/05/27 22:38:27, stevenjb wrote:
> On 2016/05/27 22:00:49, Dan Beam wrote:
> >
>
https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
> > File ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html
> > (right):
> > 
> >
>
https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
> > ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:13:
> > font-size: 92.31%;  /* Effectively 12px if the host default is 13px. */
> > On 2016/05/27 21:54:12, stevenjb wrote:
> > > On 2016/05/27 21:40:19, Dan Beam wrote:
> > > > On 2016/05/27 20:45:09, stevenjb wrote:
> > > > > 92.31% seems... fragile. Grepping the existing code I see a mix of px,
> %,
> > > and
> > > > > one use of 'em'.
> > > > > 
> > > > > No need to do this now, but I would advocate for a consistency pass. 
> > > > > 
> > > > > My experience outside of HTML suggests that explicit sets of font
sizes
> > work
> > > > > better than percentages (i.e. 92.31% may not look good if the default
> > > changes
> > > > to
> > > > > 14px or the font changes), which suggests to me that we would be
better
> > off
> > > > > using CSS variables for font sizes. That said, I have very little
> > experience
> > > > > with font sizes in HTML.
> > > > 
> > > > em and % are both scalable font-size units.  getting them consistent is
> not
> > > > really a goal of mine.  using an absolute px length here would have
> > functional
> > > > issues when the user changes their default "Web Content" font size.
> > > > 
> > > > for example: the default font-size in Chrome is 13px.  when that's
changed
> > > from
> > > > settings to 26px, any element with a hardcoded "13px" doesn't adapt and
> > looks
> > > > out of place (and may be inaccessible to users with poor vision).
> > > 
> > > So are you saying we should be using all three (px, %, and em)?
> > 
> > no, we attempt to never use px when the font-size may vary.  either % or em
> are
> > acceptable.
> > 
> > > As someone only
> > > passingly familiar with font sizing if I look at the existing code it is
> > unclear
> > > what pattern I should follow.
> > 
> > the nearby convention.
> > 
> > > 
> > > Will 92.31% still look correct if the default font size is changed to,
say,
> > > 15px? If so, would "90%" work just as well here?
> > 
> > if the user changes their default font size from 13px to 15px, I would
expect
> > tooltips' font to also change proportionally.  are you asking, "will 92.31%
x
> 15
> > be a round number?" no, not necesarilly, but I don't think that's an
> expectation
> > or really matters much.
> > 
> >
>
https://codereview.chromium.org/2019563002/diff/20001/ui/webui/resources/cr_e...
> > ui/webui/resources/cr_elements/policy/cr_policy_pref_indicator.html:14:
> > font-weight: 500;
> > On 2016/05/27 21:54:12, stevenjb wrote:
> > > On 2016/05/27 21:40:20, Dan Beam wrote:
> > > > On 2016/05/27 20:45:09, stevenjb wrote:
> > > > > We use 'bold' in a few places still, it would be good to make that
> > > consistent
> > > > at
> > > > > the same time. CSS variables seem like a good idea here too since my
> > > > > understanding is that not all font weights will be noticeably
different
> on
> > > all
> > > > > fonts (and we currently use 400, 500, and 600).
> > > > 
> > > > chrome bundles Roboto with weights of 400, 500, and 700.
> > > > 
> > > > they all look different.
> > > > 
> > > > 400 is "normal" (both in CSS and spec terms)
> > > > 500 is "medium" (spec)
> > > > 700 is "bold" (both CSS and spec terms, this weight didn't exist until
> > > recently)
> > > 
> > > What abut 600, which we currently use in bluetooth_device_dialog.html? 
> > > 
> > > > 
> > > > there was previously 300 that was called "light" in specs and used in
only
> 1
> > > > place (incognito NTP).  it was removed because it was adding size to
> chrome
> > > for
> > > > little benefit.
> > > 
> > 
> > the situation may differ slightly on ChromeOS (I think Roboto is a system
font
> > there?), but in desktop: if you use font-weight: 600; it'd just take some
> other
> > weight (i.e. 400) and interpolate the glyphs.  kind of like if you have a
> small
> > image and display it at a large size: the browser just takes its best guess
at
> > what it should look like but it generally doesn't look good nor is it
defined.
> 
> I think you misunderstand me. We *are* using 600,

I understand and am not surprised.  The web platform does not crash if you use
undefined values.  That's common.  The only real glitch you get here is slightly
blurry or bad-looking font rendering, which we can live with, but currently 600
is not included on *desktop* (and like I said: I don't know which weights you
guys bundle in ChromeOS).

> probably copied from old settings, but apparently *shouldn't* be.

It's possible.

> This is not documented anywhere. 

here's how chrome pulls in Roboto:
https://code.google.com/p/chromium/codesearch#chromium/src/ui/webui/resources...

I've also added a blurb here about % and em:
http://www.chromium.org/developers/web-development-style-guide#TOC-Basics

in general: abstraction is a double-edged sword.  roboto.css magically loads
Robot and certain weights, which is why it's hard to know how it works and which
variations are valid.

> I think that is a problem, and I think we have a similar problem with font
sizes.

eh, i think we're fairly consistent.  there are some pages that don't ever
change based on user-agent styles, and those pages can use px.

> Using 93.21% everywhere we want "slightly smaller than default" requires an
> extra comment just to make it semi readable. If you do not think this is a
> problem that is fine, obviously I do not have as much time to focus on any of
> this as I would like to, otherwise I would volunteer to help improve it :(

I'm open to any alternative method that maintains the scaling we desire (i.e.
the font gets bigger or smaller if a user changes their default font-size) but
improves readabilty.  I just don't currently know a better option.

The current options are:
- use % (which is at least semi-understood / common) or
- use em (which are less common, and basically % / 100).

Ems are useful in cases that you need to use font-size-based lengths but % is
not feasible.  For example: border-radius: .5em; yields a radius of half the
current font-size (i.e. font-size: 13px; -> border-radius: 6.5px) whereas
border-radius: 50% would give you a different result.

[michaelpg, 2016-05-27 23:07:47]

On 2016/05/27 19:28:14, Dan Beam wrote:
> On 2016/05/27 19:00:26, michaelpg wrote:
> > On 2016/05/27 02:14:52, Dan Beam wrote:
> > > whole section on mouse hover: http://i.imgur.com/owaLN2j.png
> > > when focused via Tab: http://i.imgur.com/IfBxMNr.png
> > 
> > Huh? Why, and how, is the font different between these two?
> 
> because it was before I noticed the spec asks for 12px font instead of 13px,
so
> the smaller one is the final, fixed, correct font-size

LOL, okay, I thought it was a kerning thing due to a blink issue or something.
lgtm 2.