From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 dev/build/windows/configure_profile.sh | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'dev/build/windows/configure_profile.sh')

diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 09a9cf35..16c972e8 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -1,5 +1,16 @@
 #!/bin/bash
 
+###################### COPYRIGHT/COPYLEFT ######################
+
+# (C) 2016 Intel Deutschland GmbH
+# Author: Michael Soegtrop
+#
+# Released to the public by Intel under the
+# GNU Lesser General Public License Version 2.1 or later
+# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+###################### CONFIGURE CYGWIN USER PROFILE FOR BUILDING COQ ######################
+
 rcfile=~/.bash_profile
 donefile=~/.bash_profile.upated
 
@@ -7,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
@@ -29,4 +40,4 @@ if [ ! -f $donefile ] ; then
     echo unset OCAMLLIB >> $rcfile
 
     touch $donefile
-fi
\ No newline at end of file
+fi
-- 
cgit v1.2.3