diff options
| author | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2019-02-08 15:27:19 +0000 |
|---|---|---|
| committer | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2019-02-08 15:27:19 +0000 |
| commit | 0b35f53a43aa7c712f350eecd503877502f3e0fc (patch) | |
| tree | d414f92b8d10513347238ee4923ccfcbd11b0137 | |
| parent | 34962065fb408fbd486d5765fe6a690c94ee4c8b (diff) | |
jenkins-helpers.sh: Support custom docker root dirs
Several of our machines have docker root dir set to /home/docker
instead of standard /var/lib/docker.
The reason for using /home/docker is to allocate docker containers
on the biggest disk partition.
Change-Id: I6d16f561b5b8d303cb58d3a30f2847814eb55756
| -rw-r--r-- | jenkins-helpers.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh index 57e4b4f5..487d9cff 100644 --- a/jenkins-helpers.sh +++ b/jenkins-helpers.sh @@ -672,7 +672,9 @@ print_docker_path () if [ -f "/.dockerenv" ] && mount | grep -q "/run/docker.sock "; then # If inside "host" container (with proxied docker and /home from host-home volume), # convert paths to refer to volume's path on bare-metal. - echo "$path" | sed -e "s#^/home/#/var/lib/docker/volumes/host-home/_data/#" + local docker_root + docker_root=$(docker info | grep "Docker Root Dir:" | cut -d: -f 2) + echo "$path" | sed -e "s#^/home/#$docker_root/volumes/host-home/_data/#" else echo "$path" fi |