Skip to content

Commit

Permalink
export COQ_IMAGE
Browse files Browse the repository at this point in the history
This should allow users who want to access `COQ_IMAGE` to access it by adding `COQ_IMAGE` to the `export:` list.
  • Loading branch information
JasonGross authored May 9, 2024
1 parent 0a636bc commit d7a5c76
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions entrypoint.sh
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,8 @@ docker image inspect "$COQ_IMAGE" --format="Reusing existing local image." || do

endGroup

export COQ_IMAGE

## Note to docker-coq-action maintainers: Run ./helper.sh gen & Copy min.sh
# shellcheck disable=SC2046,SC2086
docker run --pull=never -i --init --rm --name=COQ $( [ -n "$INPUT_EXPORT" ] && printf -- "-e %s " $INPUT_EXPORT ) -e WORKDIR="$WORKDIR" -e PACKAGE="$PACKAGE" \
Expand Down

0 comments on commit d7a5c76

Please sign in to comment.