> By '$HOME', I assume you mean the path of my local home directory. By
> the way, what is my $PATH? Where do I find it and how may I alter it?
"HOME" and "PATH" are so-called "environment" variables.
You can change them in the initialization files of your shell (command-line
interpreter). Which file depends on which shell you use: Try the command
"echo $SHELL" to find out.
If it is "bash", you can add something like the following lines in the
".bash_profile" file in your home directory [1]:
#---CUT---
# set PATH so it includes user's private bin if it exists
if [ -d ~/bin ] ; then
PATH=~/bin:"${PATH}"
fi
#---CUT---
Best,
Gilles
[1] You must log in again for the change to take effect.
_______________________________________________
lilypond-user mailing list
lilypond-user@gnu.org
http://lists.gnu.org/mailman/listinfo/lilypond-user
