Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

user.sh: put env settings in /etc/bash.bashrc #83

Merged
merged 1 commit into from
May 22, 2024
Merged

user.sh: put env settings in /etc/bash.bashrc #83

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 15 additions & 18 deletions scripts/utils/user.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,8 @@ EOF

mkdir "/home/${UNAME}"

# Put in some branding
# Put in some branding. This is in the volume, so it can be edited/removed by
# the user.
# shellcheck disable=SC2129
cat << EOF >> "/home/${UNAME}/.bashrc"
echo '___ '
Expand All @@ -97,29 +98,25 @@ echo ' / '
echo 'Hello, welcome to the seL4/CAmkES/L4v docker build environment'
EOF

# This is a small hack. When the dockerfiles are building, many of
# the env things are set into the .bashrc of root (since they're
# building as the root user). Here we just copy all those declarations
# and put them in this user's .bashrc.
# This can be an issue with regard to the NOTE above, about docker
# volumes.
grep "export" /root/.bashrc >> "/home/${UNAME}/.bashrc"

# Note that this block does not do parameter expansion, so will be
# copied verbatim into the user's .bashrc.
# We use this to ensure they have the repo program in their path,
# that they pick up any potentially present Haskell installation,
# and to ensure they start in the /host dir (aka, their own file
# path)
cat << 'EOF' >> "/home/${UNAME}/.bashrc"
# Since the user home is mounted as a volume, we do not write to ~/.bashrc, but
# modify the system-wide bashrc instead. /etc/profile.d/ does not work, because
# it's not a login shell.
#
# When the dockerfiles are building, many of the env settings are written into
# /root/.bashrc by various install tools. We copy all those declarations.
RC_FILE="/etc/bash.bashrc"
grep "export" /root/.bashrc >> "${RC_FILE}"

# The following are in addition to the declarations in /root/.bashrc. Note that
# this block does not do parameter expansion, so will be copied verbatim.
cat << 'EOF' >> "${RC_FILE}"
export PATH=/scripts/repo:$PATH
export GHCUP_INSTALL_BASE_PREFIX=/opt/ghcup
[ -r /opt/ghcup/.ghcup/env ] && source /opt/ghcup/.ghcup/env
cd /host
EOF

# Set an appropriate chown setting, based on if the group setup
# went OK
# Set an appropriate chown setting, based on if the group setup went OK
chown_setting="${UNAME}"
if [ "$GROUP_OK" = true ]; then
chown_setting="${UNAME}:${GROUP}"
Expand Down