mirror of
https://github.com/paparazzi/paparazzi.git
synced 2026-05-09 22:49:53 +08:00
Felix Ruess
85fa26e6d3
- Update to Ubuntu xenial and switch to new gcc-arm-embedded PPA. - Hhandle permissions for docker volumes by dynamically changing the id of user pprz to LOCAL_USER_ID. This should finally make it possible use the shared volume with the paparazzi source in docker on machines where your user/group id is not 1000
27 lines
986 B
Bash
Executable File
27 lines
986 B
Bash
Executable File
#!/bin/bash
|
|
|
|
# If user exists, change user and group ids, otherwise add new local user
|
|
# Either use the LOCAL_USER_ID if passed in at runtime or
|
|
# fallback
|
|
|
|
USER_NAME=${USERNAME:-pprz}
|
|
USER_ID=${LOCAL_USER_ID:-1000}
|
|
GROUP_ID=${LOCAL_GROUP_ID:-1000}
|
|
|
|
if id -u $USER_NAME > /dev/null 2>&1; then
|
|
echo "Starting with UID: $USER_ID and GID: $GROUP_ID"
|
|
# modify existing pprz user instead of creating new one
|
|
#usermod -o --uid $USER_ID $USER_NAME
|
|
groupmod -o --gid $GROUP_ID $USER_NAME
|
|
# usermod goes through all files in home dir and changes the userid, which takes a while
|
|
# since we don't want/need that here, directly change the user id in /etc/passwd
|
|
sed -i "s/$USER_NAME:x:\([0-9]*\):\([0-9]*\):/$USER_NAME:x:$USER_ID:\2:/g" /etc/passwd
|
|
else
|
|
echo "Adding new user $USER_NAME with UID: $USER_ID and GID: $GROUP_ID"
|
|
useradd --shell /bin/bash -u $USER_ID -o -c "" -m $USER_NAME
|
|
fi
|
|
|
|
export HOME=/home/$USER_NAME
|
|
|
|
exec /usr/local/bin/gosu $USER_NAME "$@"
|