diff options
Diffstat (limited to 'dev/build/windows/configure_profile.sh')
| -rw-r--r-- | dev/build/windows/configure_profile.sh | 15 |
1 files changed, 13 insertions, 2 deletions
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 |