GNU bug report logs - #52303
[PATCH] Remove not defined face info-menu-5 from manoj-dark theme

Previous Next

Full log

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Y. E. <yet <at> ego.team>
To: bug-gnu-emacs <at> gnu.org
Subject: [PATCH] Remove not defined face info-menu-5 from manoj-dark theme
Date: Sun, 05 Dec 2021 19:43:55 +0200

[Message part 1 (text/plain, inline)]

Tags: patch

Hello,

The face 'info-menu-5' was obsoleted in favor to 'info-menu-star' back
in 2005 (185cff95450).

This patch suggests removal of the not defined face and not updating it,
because the de facto used 'info-menu-star' default value has served the
theme users during the last years.

A side-question: do I still need to add "Copyright-paperwork-exempt:
yes" to the minor commits even if I have the CA completed?

Thanks,
YE

[0001-etc-themes-manoj-dark-theme.el-Remove-not-defined-fa.patch (text/patch, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.