diff --git a/dev-install.sh b/dev-install.sh index 9dc0de2..a925843 100755 --- a/dev-install.sh +++ b/dev-install.sh @@ -3,20 +3,28 @@ set -e vagrant up -host=$(vagrant ssh-config | awk '{ if ($1 == "HostName") { print($2) }}') -port=$(vagrant ssh-config | awk '{ if ($1 == "Port") { print($2) }}') -key=$(vagrant ssh-config | awk '{ if ($1 == "IdentityFile") { print($2) }}') + +if [ -z "$http_proxy" ]; then + http_proxy=$(vagrant ssh -- sh -c '. /etc/profile.d/http_proxy.sh 2>/dev/null; echo $http_proxy') +fi + +if [ -z "$http_proxy" ]; then + printf "HTTP Proxy[none]: " + read http_proxy +fi if [ -n "$http_proxy" ]; then - proxy="\"command_prefixes\": [\"http_proxy='$http_proxy'\"]," -else - proxy= + vagrant ssh -- sudo /vagrant/proxy.sh $http_proxy + export http_proxy fi +host=$(vagrant ssh-config | awk '{ if ($1 == "HostName") { print($2) }}') +port=$(vagrant ssh-config | awk '{ if ($1 == "Port") { print($2) }}') +key=$(vagrant ssh-config | awk '{ if ($1 == "IdentityFile") { print($2) }}') + cat > colab/environments.json < /etc/profile.d/http_proxy.sh<