Created raspberrypi/pico-sdk-tools#21 (maybe wait what happens with raspberrypi/pico-sdk#2484 as well).