Docker Clues
Known good platforms: ubuntu 20.04, ubuntu 18.04 Get the docker package (s) (see https://docs.docker.com/get-docker/) Install docker Add user to docker group in /etc/group Check groups : should see docker (may have to logout and login again!) mkdir a directory get the image get the script initial pass: cd directory ./docker.sh init nth pass: ./docker.sh run NOTE: You might see an error message like this, when you type ./docker.sh run docker run -it -u=1000:1000 --name opencilk --rm -v /home/xxx/cilk/mtest/tutorial:/tutorial pact2021tutorial:20210927 groups: cannot find name for group ID 1000 I have no name!@ef590f4b3de6:/$ PLEASE IGNORE THIS ERROR cd /tutorial Editting - maybe edit inside docker image? YMMV - maybe exit from docker image; edit; ./docker.sh run - maybe have an extra window: cd directory do editting To exit a docker session started by "./docker.sh run" type exit