diff --git a/docker/admin/install.bash b/docker/admin/install.bash index ee71495..5c63c81 100755 --- a/docker/admin/install.bash +++ b/docker/admin/install.bash @@ -31,6 +31,7 @@ EOF packages=" apt-file +clang dctrl-tools docker-ce-cli g++ diff --git a/tools/ci-run.bash b/tools/ci-run.bash index 86cb7af..f3d0600 100755 --- a/tools/ci-run.bash +++ b/tools/ci-run.bash @@ -4,5 +4,5 @@ set -euo pipefail echo "${DOCKER_PASSWORD}" | sudo -E docker login --username "${DOCKER_USERNAME}" --password-stdin -make shell I=runtime CMD="make system" +make system make publish Z=1