Anmol Sethi 9fb318cf15 docker: Fix $DOCKER_USER (#2057) ...

We do not try renaming $HOME anymore as there is no good way
to do it.

We also only try to convert if the user hasn't been changed.

Finally I added usage to the docker docs in install.md

Closes #2056

2020-09-03 18:38:40 -04:00

1.4 KiB

Raw Blame History

View Raw