Cannot use pintos by ssh

Question

I use a docker container to try pintos on my mac(M1). Everything behaves well when I start the container by docker start -i pintos.

However, when I use ssh to connect my docker container(i.e., ssh -p xxxx root@local), error message -bash: pintos: command not found occurs if I try pintos -- in directory /pintos/src/threads/build.

Answer 1

Make sure the pintos executable is in your $PATH. Type

$ echo $PATH

and make sure the pintos binary is located in one of the folders listed. If not add the executable to your PATH (as described here: How to permanently set $PATH on Linux/Unix) or write the full path to it.