Currently Dune container is always named dune_container, we should allow a customized name such as container_dev, container_prod, container_smith, container_mmddyyyy picked by end-users.
An easy implementation is to add an option for ./dune, which will call 'docker rename dune_container customizedName'
Once container name is changed, we need take care of the places of DUNE where dune_container is hard-coded such as tests/ etc.
Currently Dune container is always named dune_container, we should allow a customized name such as container_dev, container_prod, container_smith, container_mmddyyyy picked by end-users.
An easy implementation is to add an option for ./dune, which will call 'docker rename dune_container customizedName'
Once container name is changed, we need take care of the places of DUNE where dune_container is hard-coded such as tests/ etc.