From d7a5c76d3b779d5188cb3be0edee5902e6a17f98 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 9 May 2024 15:07:16 -0700
Subject: [PATCH] export COQ_IMAGE

This should allow users who want to access `COQ_IMAGE` to access it by adding `COQ_IMAGE` to the `export:` list.
---
 entrypoint.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/entrypoint.sh b/entrypoint.sh
index 6d2ab2e..966f516 100755
--- a/entrypoint.sh
+++ b/entrypoint.sh
@@ -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" \