[docker] update docker instance name

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} $@