diff options
author | Andrei Karas <akaras@inbox.ru> | 2016-06-11 22:19:12 +0300 |
---|---|---|
committer | Andrei Karas <akaras@inbox.ru> | 2016-06-11 22:19:12 +0300 |
commit | e17646d427bc5c56836b178bcdb5ba6cd34217f4 (patch) | |
tree | f61940230763a854c28cb0ae4a82ce2906126e3e | |
parent | f791f3b8ec8f784c4c04249d4b5e3fba87751829 (diff) | |
download | plus-e17646d427bc5c56836b178bcdb5ba6cd34217f4.tar.gz plus-e17646d427bc5c56836b178bcdb5ba6cd34217f4.tar.bz2 plus-e17646d427bc5c56836b178bcdb5ba6cd34217f4.tar.xz plus-e17646d427bc5c56836b178bcdb5ba6cd34217f4.zip |
In ci scripts use local debian mirror if run on local runner.
-rwxr-xr-x | tools/ci/scripts/init.sh | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index fa407371b..b64fa7fb1 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -17,6 +17,16 @@ function do_init { check_error $? } +function update_repos { + export DATA=$(cat /etc/resolv.conf|grep "nameserver 1.10.100.101") + echo "${DATA}" + if [ "$DATA" != "" ]; + then + echo "Detected local runner" + sed -i 's!http://httpredir.debian.org/debian!http://1.10.100.103/debian!' /etc/apt/sources.list + fi +} + function aptget_update { echo "apt-get update" apt-get update @@ -210,4 +220,5 @@ function run_mplint { run_check_warnings } +update_repos aptget_update |