On Fri, 9 Feb 2018, Sven Schreiber wrote:
Hm, I'm still having no luck. Perhaps it has to do that newly
downloaded .sh
files get a number extension and thus the correct files are not being
executed. I will try to clean up everything and start more or less from
scratch.
That behavior of wget can be confusing. But you can use the -N option
to make it overwite a previously downloaded file when the remote
version is newer, as in
wget -N
http://ricardo.ecn.wfu.edu/pub/gretl/winbuild/texinst.sh
Allin