I decommented and edited the two lines in
/etc/default/grub which are relative to the colors, as follows
then I've run
sudo grub-mkconfig -o /boot/grub/grub.cfg and reboot. Strangely it seems that only the second line had effect.
On the other hand, when I hit C on GRUB's main screen and get the console, then I can enter, for instance,
set color_normal=yellow/blue and
set color_highlight=red/cyan and verify that both commands had effect (after going back to GRUB's main screen by hitting Esc).
I've also tried to put those two lines just before
if [ x$GRUB_COLOR_NORMAL != x ] && [ x$GRUB_COLOR_HIGHLIGHT != x ] ; then cat << EOF set menu_color_normal=$GRUB_COLOR_NORMAL set menu_color_highlight=$GRUB_COLOR_HIGHLIGHT EOF fi
/etc/grub.d/00_header, thinking that
/etc/default/grub could be overridden by this latter file, but it still has no effect.