mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-26 22:29:08 +03:00
make message more obvious
This commit is contained in:
parent
6247bbfd59
commit
f87198806b
@ -20,6 +20,8 @@ tasks:
|
|||||||
ssh-keygen -q -t rsa -N '' -f ~/.ssh/id_rsa
|
ssh-keygen -q -t rsa -N '' -f ~/.ssh/id_rsa
|
||||||
echo
|
echo
|
||||||
SSH_KEY=~/.ssh/id_rsa.$(basename $(gp url))
|
SSH_KEY=~/.ssh/id_rsa.$(basename $(gp url))
|
||||||
|
echo "Paste the below script into your local shell to connect."
|
||||||
|
echo "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv"
|
||||||
echo "cat <<EOF >$SSH_KEY"
|
echo "cat <<EOF >$SSH_KEY"
|
||||||
cat ~/.ssh/id_rsa
|
cat ~/.ssh/id_rsa
|
||||||
echo "EOF"
|
echo "EOF"
|
||||||
@ -33,8 +35,8 @@ tasks:
|
|||||||
echo "ssh \\"
|
echo "ssh \\"
|
||||||
echo " -o ProxyCommand='chisel client $(gp url 8080) stdio:%h:%p' \\"
|
echo " -o ProxyCommand='chisel client $(gp url 8080) stdio:%h:%p' \\"
|
||||||
echo " gitpod@localhost -p 2222"
|
echo " gitpod@localhost -p 2222"
|
||||||
echo
|
echo "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^"
|
||||||
echo "To connect from your local machine, paste the above script into your local shell."
|
echo "Paste the above script into your local shell to connect."
|
||||||
ports:
|
ports:
|
||||||
- port: 8080
|
- port: 8080
|
||||||
- port: 2222
|
- port: 2222
|
||||||
|
Loading…
Reference in New Issue
Block a user