SIGN IN SIGN UP

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
A
Anmol Sethi committed
9fb318cf15191f2766c39e5d1eb549ff11ca1487
Parent: 4a250be
Committed by GitHub <noreply@github.com> on 9/3/2020, 10:38:40 PM