Open
Description
If a board header file includes other header files, then CMake does not see any pico_cmake_set directives in the secondary header file.
This particularly affects the vgaboard.h header file, which includes pico.h. None of the pico settings are seen by CMake. This does not matter in this case as all the settings are default values anyway.
However, it is not possible to simply change pico.h to pico2.h for a VGA board with pico2 installed, as CMake will still think it is compiling for RP2040 rather than RP2350.