diff --git a/scripts/run-docker.sh b/scripts/run-docker.sh index 10e4623aeb264cab08730db03a943954b7345510..9d97b2596da3b15eced69a762df0f3e78dc16804 100755 --- a/scripts/run-docker.sh +++ b/scripts/run-docker.sh @@ -6,7 +6,7 @@ # usage function usage () { echo "Usage: " $0 " [-h|--help] [-i|--id ID] [-t|--tmp TMP_DIR] [options passed to docker]" - echo " Run a docker instance named \"lustrec_docker\" built with image " $CONTAINER_ID " by default." + echo " Run a docker instance named \"lustrec_docker_run\" built with image " $CONTAINER_ID " by default." echo " Available options:" echo " - [-i|--id ID] | change container image ID" echo " - [-t|--tmp TMP_DIR] | change binding for /tmp dir in container. Default to /tmp" @@ -54,6 +54,6 @@ done # launch docker docker run -it --rm \ - --name "lustrec-from-${CONTAINER_ID}" \ + --name "lustrec_docker_run" \ -v ${TMP_DIR}:/tmp -v ${PWD}:/home/opam/lustrec \ ${CONTAINER_ID} $@