diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /dev/build/windows/configure_profile.sh | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
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 |