3 commits

Author	SHA1	Message	Date
Anmol Sethi	eacca7d692	Unrelated fixes for CI	2020-10-07 15:58:30 -04:00
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
Anmol Sethi	4c4a7413a1	docker: Allow passing $DOCKER_USER to set the username in the container ... Needs to be reflected in the documentation and the dockerhub description now. Closes #881	2020-08-27 14:20:56 -04:00