bug#31131: 26.1; menu-set-font not setting font properly and artefacts on bold face

[Eli Zaretskii]

> From: Benjamin Andresen <benny@in-ulm.de>
> Cc: 31131@debbugs.gnu.org
> Date: Thu, 12 Apr 2018 22:00:23 +0200
> 
> Eli Zaretskii <eliz@gnu.org> writes:
> > Then please send snapshots of the problematic display, maybe it 
> > will
> > give a clue.  Because I couldn't see the video you posted.
> 
> I've uploaded an imgur.com album with 1 frame per second.
> https://imgur.com/a/03JUB

You mean, the slightly yellowish color of some of the text where the
cursor was moved?  I'm quite sure this is something local to your
system, like some problem with your video driver.  If the driver
software has some "acceleration" or "advanced" features, try turning
them off.

> (Not sure if attachments work on debbugs.)

They certainly do, and doing so is the preferred way of showing
images, because this way the images get filed by the bug tracker and
will be available regardless of what imgur does with their cleanup
policies.

Thanks.