Google ChromeOS specific options were shown in the main menu
unconditionally, even on non-ChromeOS devices. Instead, hide
these options unless CONFIG_CHROMEOS is set, and also put them
in a separate menu.
Change-Id: I75f533ed5046d6df4f7d959a0ca4c2441340ef2f
Signed-off-by: Stefan Reinauer <reinauer@google.com>
Reviewed-on: http://review.coreboot.org/848
Reviewed-by: Martin Roth <martin@se-eng.com>
Tested-by: build bot (Jenkins)
Reviewed-by: Mathias Krause <minipli@googlemail.com>
f17789c4ff