My description verbatim from a post to the EdLUG e-mail list:
> Second, and possibly related weirdness, is that I've got a shell script with
> read and execute perms in /usr/local/bin. My PATH contains /usr/local/bin,
> and I can get the name of the script using command-completion.
>
> But when I execute it, I get the following from bash:
>
> bash: /usr/bin/proofgeneral: No such file or directory
>
> I've checked, it's just not executing the script. I think that the
> command-completion part is telling bash that it's in /usr/bin, rather than
> where it really is.
>
> Thing is that other scripts in /usr/local/bin do not have this problem. (One
> of them is a script that runs Proof General.)
>
> If I give the fill path, /usr/local/bin/proofgeneral, then it runs fine.
As it turns out, commenting-out the use of /etc/bash_completion in my .bashrc file fixes this.
Here's the kicker: I'm not even using completion. I just type in the full name, and bash_completion mucks it up somewhere and says that it's in a different location.
FYI, the version of ProofGeneral that I cam using comes from
http://www.cl.cam.ac.uk/research/hvg/Isabelle/installation.html#install_linux
and I've installed it in /usr/local/share.
I forgot to add that if I sudo, then it works fine. Presumably because arguments to sudo are handled differently, not because this is a permissions issue.