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
..
Dockerfile	docker: Fix $DOCKER_USER (#2057)	2020-09-03 18:38:40 -04:00
build.sh	Rename container and release-container to images and release-image	2020-06-03 15:45:16 -04:00
entrypoint.sh	docker: Fix $DOCKER_USER (#2057)	2020-09-03 18:38:40 -04:00