Subject: Re: bug#24107: 25.1; menu-bar-size and tool-bar-size are reported inconsistently on w32

From: martin rudalics <[email-masked]>
Date: Sat, 30 Jul 2016 14:30:32 +0200

> Yes, thanks.

Installed on master.  Bug closed.

Thanks for spotting this blatant discrepancy, martin