Hey guys, this one just needs a one-line fix somewhere:

Problem

When using

#include "boot/picobin.h"

before any other includes, this compilation error is emitted:

/usr/local/pico-sdk/src/rp2350/pico_platform/include/pico/platform.h:20:2: error: #error pico/platform.h should not be included directly; include pico.h instead
   20 | #error pico/platform.h should not be included directly; include pico.h instead

This is initially confusing, however, because the user obviously didn't try to include pico/platform.h directly. Furthermore, including pico.h directly instead (the solution indicated) does not actually cause the inclusion of boot/picobin.h.

Expected Outcome

If boot/picobin.h is intended to be included directly by the user, it should include its own dependencies. (As it's included directly here I'm assuming that's the case.) Otherwise, it should emit an error identifying a header that can be included that includes boot/picobin.h, after including its dependencies.