dot_bash_profile

# Any copyright is dedicated to the Public Domain.
# https://creativecommons.org/publicdomain/zero/1.0/

add_to_path() {
    if [[ ! ":$PATH:" == *":$1:"* ]]; then
        export PATH="$PATH:$1"
    fi
}

add_to_path "$HOME/.local/bin"
add_to_path "$HOME/.cargo/bin"
add_to_path "$HOME/.local/gems/bin"

source ~/.bashrc

# opam configuration
test -r /home/steveno/.local/share/opam/opam-init/init.sh && . /home/steveno/.local/share/opam/opam-init/init.sh > /dev/null 2> /dev/null || true