# /var/etc/profile.local: your profile modifications for the shell