From 80d107005be955abc5b7605e803f1b21451618d0 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Fri, 9 Jun 2017 14:46:46 +0200
Subject: Fix proxy setting issue

---
 dev/build/windows/MakeCoq_regtest_noproxy.bat | 2 +-
 dev/build/windows/configure_profile.sh        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

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
-- 
cgit v1.2.3