diff options
Diffstat (limited to '')
| -rw-r--r-- | .bash_profile | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.bash_profile b/.bash_profile index fef0e14..027c569 100644 --- a/.bash_profile +++ b/.bash_profile @@ -8,3 +8,6 @@ export PATH [[ -f ~/.bashrc ]] && . ~/.bashrc source ~/.setup/.bash_profile.local + +# opam configuration +test -r /home/benj/.opam/opam-init/init.sh && . /home/benj/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true |
