On the advice to source .profile in .bashrc.

[dbuenzli]

I know people like @AltGr banged their head on the table quite a bit with these things. But I'm wondering whether this:

Do you want opam to modify ~/.profile? [N/y/f]
(default is 'no', use 'f' to choose a different file) y

User configuration:
  Updating ~/.profile.
[NOTE] Make sure that ~/.profile is well sourced in your ~/.bashrc.

is good advice. I just installed a bare debian (bookworm) on a pi and .profile has:

# if running bash
if [ -n "$BASH_VERSION" ]; then
    # include .bashrc if it exists
    if [ -f "$HOME/.bashrc" ]; then
	. "$HOME/.bashrc"
    fi
fi

by default. (I also checked a few servers I manage that have earlier debian version and they all seem to have similar runes in the .profile).

So if you source your .profile in .bashrc you create an infinite loop and ssh quicks you out. Shouldn't opam rather add the rune to .bashrc and tell that you should make sure that .bashrc is well sourced from .profile :-) ?

[kit-ty-kate]

Note for opam devs from the dev meeting: We currently don't differenciate between POSIX shell and bash. I think we should probably have a different case for bash and this way we can support it properly