diff options
Diffstat (limited to 'dist')
| -rwxr-xr-x | dist/ci-run.sh | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/dist/ci-run.sh b/dist/ci-run.sh index 43e1c8b66..cee5d05e2 100755 --- a/dist/ci-run.sh +++ b/dist/ci-run.sh @@ -407,7 +407,13 @@ ci_run () { gend printf "$ANSI_BLUE[CI] Build ghdl in docker image ghdl/build:$BUILD_IMAGE_TAG\n" - $RUN -e GHDL_DESC="$(git describe --dirty)@${BUILD_IMAGE_TAG}" -e CONFIG_OPTS="$CONFIG_OPTS" "ghdl/build:$BUILD_IMAGE_TAG" bash -c "${scriptdir}/ci-run.sh $BUILD_CMD_OPTS build" + $RUN \ + -e GHDL_VER_DESC="$(git describe --dirty)" \ + -e GHDL_VER_REF="$(git rev-parse --abbrev-ref HEAD)@${BUILD_IMAGE_TAG}" \ + -e GHDL_VER_HASH="$(git rev-parse HEAD)" \ + -e CONFIG_OPTS="$CONFIG_OPTS" \ + ghdl/build:"$BUILD_IMAGE_TAG" \ + bash -c "${scriptdir}/ci-run.sh $BUILD_CMD_OPTS build" fi if [ ! -f build_ok ]; then |