diff options
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 |