I wrote
I found no way to get the download script to run the bash script: I
had to manually 'source' it instead. I never worked out why.
(Perhaps a security feature in bash?)
It turns out the 'Perhaps' guess was correct. Bash scripts are prevented
from simply running bash scripts in the current directory: various users
have raised questions about this posted online and various workarounds
exist. But changing the invoked script to use tcsh works and is simpler
than any of the solutions I found online. Perhaps there is some reason why
that should not be done.
Aaron
