Skip to content

On the advice to source .profile in .bashrc. #5819

@dbuenzli

Description

@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 :-) ?

Metadata

Metadata

Assignees

No one assigned

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions