diff --git a/doc/Dockerfile b/doc/Dockerfile index 76f88ad77c..e18fc008e5 100644 --- a/doc/Dockerfile +++ b/doc/Dockerfile @@ -14,14 +14,13 @@ # Run the docker image: # $ docker images # $ export DOCKER_IMAGE_ID= docker images | awk '{print $3}'|head -n2 | tail -n1` -# $ docker -ti ${DOCKER_IMAGE_ID} bash +# $ docker run -ti ${DOCKER_IMAGE_ID} bash # # Once you quit the bash session get the container id with: # $ docker ps -a | grep bash # # To get into that shell again just type: -# $ docker start -# $ docker attach +# $ docker start -ai # # To share those images: # $ docker export | xz > container.xz