cd into home/pintos git init git remote add origin |ssh-url| mv src src-old. (rename src) git fetch git pull origin main git checkout main rm -rf src mv src-old src