Skip to content

Changes

Summary

  1. jobs/coverity: adjust mount path to new home dir (details)
Commit 6a2451a0ad3dd2f5e3179d64446d9d553a37016d by Oliver Smith
jobs/coverity: adjust mount path to new home dir

With the related docker-playground patch, the home dir for the build
user has actually been changed from /home/build to /build. This doesn't
matter for all other jobs it seems, but the coverity job here fails
because it tries to access $HOME/osmo-ci/coverity.

Adjust the mount path, so it works again as expected.

Fix for:
  ./jenkins.sh: line 37: /build/osmo-ci/coverity/get_token.sh: No such file or directory

Related: docker-playground Ief8837bd9f89f51e66857a453f7fc4645620159f
Change-Id: If0286e10d1644464e9408db1bbf18c24f4b8d5a6
The file was modified jobs/coverity.yml