Surely just removing the tool from the path for that one session is absolutely fine - it's not like it's global.
For instance adding the command:
export PATH=`echo $PATH | sed -e "s/:[^:]*arm[^:]*:/:/"`
to your script would remove any path entry containing the text arm, just for that terminal session, and not across your whole system
(you probably want to run echo $PATH first to check that's the correct entry to remove though)
© Espruino, powered by microcosm.
Report a problem