bug#50424: 27.2; Tab bar button mouse face not clearing entirely

[Eli Zaretskii <eliz@gnu.org>]

> Date: Wed, 8 Sep 2021 17:57:50 +0100
> From: Alan Third <alan@idiocy.org>
> Cc: luangruo@yahoo.com, juri@linkov.net, 50424@debbugs.gnu.org
> 
> I think all it's doing is ensuring the total area the image takes up
> is the same whether there's a relief or not.
> 
> The total width = image + relief width + margin width, so if you
> reduce the size of the relief you have to increase the size of the
> margin by the same amount to make sure it takes up the same amount of
> space and doesn't move.
> 
> As far as I can see, what's happening here is that the margin is
> pushing the relief one pixel into the separator to the left, so I
> suspect that's why it's not being cleared.
> 
> I'm somewhat surprised that it's not pushing the right hand side one
> pixel too far in the other direction and causing it to not be cleared
> either, but maybe that's just chance.
> 
> The change below fixes it here, but I've not made sure it does the
> right thing with different sized margins and so on.

Thanks, I installed this, since it fixes at least the default case.