Subject: Re: bug#52303: [PATCH] Remove not defined face info-menu-5 from manoj-dark theme

From: Y. E. <[email-masked]>
Date: Tue, 07 Dec 2021 12:18:09 +0200

Hi Lars,

The pushed commit message caught my attention: it seems both the
suggested commit message and the corrected one got into.

See d3d8a6ccda7, and also 0d8e9588e1c, 6620d03e334.