diff options
| author | Michael Soegtrop | 2017-06-09 14:46:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-26 08:02:24 +0200 |
| commit | 80d107005be955abc5b7605e803f1b21451618d0 (patch) | |
| tree | ce570d0e1eee70d54e64d891d516e53fc20baa1b /dev | |
| parent | e37a6d70f5964ba773ad52efeb0a079bd5d51894 (diff) | |
Fix proxy setting issue
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/build/windows/MakeCoq_regtest_noproxy.bat | 2 | ||||
| -rw-r--r-- | dev/build/windows/configure_profile.sh | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat index bc3bce5913..7b17e721b3 100644 --- a/dev/build/windows/MakeCoq_regtest_noproxy.bat +++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat @@ -12,7 +12,7 @@ REM ========== BUILD COQ ========== call MakeCoq_SetRootPath
SET HTTP_PROXY=
-EXPORT HTTP_PROXY=
+SET HTTPS_PROXY=
MKDIR C:\Temp\srccache
call MakeCoq_MinGW.bat ^
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh index 7b9cdab0f5..0b61a31e7f 100644 --- a/dev/build/windows/configure_profile.sh +++ b/dev/build/windows/configure_profile.sh @@ -18,7 +18,7 @@ if [ ! -f $donefile ] ; then echo >> $rcfile - if [ -n "$1" ]; then + if [ "$1" != "" -a "$1" != " " ]; then echo export http_proxy="http://$1" >> $rcfile echo export https_proxy="http://$1" >> $rcfile echo export ftp_proxy="http://$1" >> $rcfile |