mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Update .gitpod.yml
This commit is contained in:
parent
f9f946096a
commit
568e7b5820
20
.gitpod.yml
20
.gitpod.yml
@ -10,12 +10,7 @@ tasks:
|
||||
dropbear -r /workspace/dropbear.hostkey -F -E -s -p 2222 -P ~/dropbear.pid
|
||||
- command: |
|
||||
mkdir -p ~/.ssh && code ~/.ssh/authorized_keys
|
||||
clear
|
||||
echo "=============="
|
||||
echo " INSTRUCTIONS "
|
||||
echo "=============="
|
||||
echo ""
|
||||
echo "1. Add your public SSH key to ~/.ssh/authorized_keys of this Gitpod workspace"
|
||||
echo "1. Add your public SSH key to the SSH_KEY environment variable before laun"
|
||||
echo ""
|
||||
echo "2. Install Chisel on your local machine, e.g. curl https://i.jpillora.com/chisel! | bash"
|
||||
echo " see https://github.com/jpillora/chisel"
|
||||
@ -23,6 +18,19 @@ tasks:
|
||||
echo "3. Connect via SSH from your local machine:"
|
||||
echo " ssh -o ProxyCommand='chisel client $(gp url 8080) stdio:%h:%p' gitpod@localhost -p 2222"
|
||||
echo ""
|
||||
- command: |
|
||||
mkdir -p ~/.ssh
|
||||
if test -z "$SSH_KEY"; then
|
||||
echo "Warning: SSH_KEY not set, skipping SSH setup"
|
||||
else
|
||||
echo "$SSH_KEY" >> ~/.ssh/authorized_keys
|
||||
echo "1. Install Chisel on your local machine, e.g. curl https://i.jpillora.com/chisel! | bash"
|
||||
echo " see https://github.com/jpillora/chisel"
|
||||
echo ""
|
||||
echo "2. Connect via SSH from your local machine:"
|
||||
echo " ssh -o ProxyCommand='chisel client $(gp url 8080) stdio:%h:%p' gitpod@localhost -p 2222"
|
||||
echo ""
|
||||
done
|
||||
ports:
|
||||
- port: 8080
|
||||
- port: 2222
|
||||
|
Loading…
Reference in New Issue
Block a user