This trick with the EXTERNAL_UID does not seem to be needed now that we don't...
requested to merge 39-current_uid-is-set-in-the-docker-container-launch-script-this-should-be-unnecessary-and-is into master
This trick with the EXTERNAL_UID does not seem to be needed now that we don't use the external user's git configuration.
Closes #39 (closed)