Closed tom93 closed 4 years ago
On Ubuntu < 19.10, sudo preserves $HOME by default (see https://askubuntu.com/a/1187000).
As a result, commands such as sudo -u domjudge make target run make as user domjudge but leave $HOME as /root.
sudo -u domjudge make target
This causes problems; for example sphinx-build -b pdf . build/team fails with the following error message:
sphinx-build -b pdf . build/team
[ERROR] pdfbuilder.py:149 [Errno 13] Permission denied: '/root/.rst2pdf/cover.tmpl'
Composer also warns about the cache directory not being writable.
The -H (--set-home) option overrides sudo's default behaviour and sets $HOME to the home directory of the target user, fixing the problems.
-H
--set-home
Thanks! This also begs the question whether we can update to 20.04. I will investigate
Yep seems to work. I just pushed a 20.04 image to Docker Hub.
On Ubuntu < 19.10, sudo preserves $HOME by default (see https://askubuntu.com/a/1187000).
As a result, commands such as
sudo -u domjudge make target
run make as user domjudge but leave $HOME as /root.This causes problems; for example
sphinx-build -b pdf . build/team
fails with the following error message:Composer also warns about the cache directory not being writable.
The
-H
(--set-home
) option overrides sudo's default behaviour and sets $HOME to the home directory of the target user, fixing the problems.