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