From 68bca0dbff232c2cdc19e9da0265e97bdd5d5d2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Tue, 7 Mar 2017 00:27:48 +0100 Subject: [PATCH] Bash profile: fix opam --- files/.bash_profile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/files/.bash_profile b/files/.bash_profile index b4feca6..dd1d70d 100644 --- a/files/.bash_profile +++ b/files/.bash_profile @@ -1,3 +1,6 @@ #!/bin/bash [ -f ~/.bashrc ] && source ~/.bashrc + +# OPAM configuration +. /home/tobast/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true