Description
On page 4 of "Getting started with Raspberry Pi Pico" there is a command to get the current copy of pico_setup.h:
wget https://raw.githubusercontent.com/raspberrypi/pico-setup/master/pico_setup.sh
It works correctly the first time, you will get:
pico_setup.sh
However, if you run it again to reinstall, you will get:
pico_setup.sh (version when first downloaded)
pico_setup.sh.1 (current version)
From the wget man page:
When running Wget without -N, -nc, -r, or -p, downloading the
same file in the same directory will result in the original
copy of file being preserved and the second copy being named
file.1.
The instructions in "Getting started with Raspberry Pi Pico" and/or the pico_setup.sh seem fragile, I had to re-install to get the SDK to work properly, which is how I discovered this. It's important to fix this, as any changes to pico_setup.sh on github won't be used if the manual's instructions had been previously followed.
I'd also suggest a "clean install" section be added to the document.
A further test for the developer of the script would be to compare the filesystem of a first install to a second install to see if there are any other cases like this.