Grub bug report / feature request

[Ron]

Greetings,

grub.cfg supports 3 colour options:

set menu_color_normal
set menu_color_highlight
set color_normal


However, /etc/default/grub only supports 2:

GRUB_COLOR_NORMAL
GRUB_COLOR_HIGHLIGHT


I'd like to propose that grub supports the 3rd "set" option, and 
further, that it be named such that it's clear that it is not referring 
to a "menu" item colour (GRUB_COLOR_NORMAL refers to menu_color_normal).


I'm using version "grub-mkconfig (GRUB) 2.02~beta2" on a Manjaro 
distribution.

Finally, to show that there *appears* to be only 2 recognized colour 
options in grub-mkconfig, I run the following:

> grep -i color $(which grub-mkconfig)
>   GRUB_COLOR_NORMAL \
>   GRUB_COLOR_HIGHLIGHT \


Thank you for your time and for grub in general.

Ronald Barnes