From 68d353b51bececbaae8a70512da00ccce370aadd Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 11 May 2024 01:07:01 +0200 Subject: [PATCH] fix: rhs path --- entrypoint.sh | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/entrypoint.sh b/entrypoint.sh index 450d534..d655f88 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -29,10 +29,13 @@ echo "RUNNER_WORKSPACE=$RUNNER_WORKSPACE" # We want to bind-mount the dirname of $GITHUB_ENV. # $GITHUB_ENV is typically /home/runner/work/_temp/_runner_file_commands/set_env_87406d6e-4979-4d42-98e1-3dab1f48b13a # so $(dirname "$GITHUB_ENV") is typically /home/runner/work/_temp/_runner_file_commands on the host. -# We also notice that $RUNNER_WORKSPACE is typically /home/runner/work/${GITHUB_REPOSITORY#*/} (e.g. /home/runner/work/docker-coq-action). +# We also notice that $RUNNER_WORKSPACE is typically /home/runner/work/${GITHUB_REPOSITORY%/*} (e.g. /home/runner/work/docker-coq-action). # Hence this hardcoded yet as-general-as-possible path: -DIR_GITHUB_RUNNER_FILE_COMMANDS="${RUNNER_WORKSPACE%/*}/_temp/_runner_file_commands" -echo "DIR_GITHUB_RUNNER_FILE_COMMANDS=$DIR_GITHUB_RUNNER_FILE_COMMANDS" +HOST_GITHUB_RUNNER_FILE_COMMANDS="${RUNNER_WORKSPACE%/*}/_temp/_runner_file_commands" +# Another hardcoded path: +DIR_FILE_COMMANDS="/github/file_commands" +echo "HOST_GITHUB_RUNNER_FILE_COMMANDS=$HOST_GITHUB_RUNNER_FILE_COMMANDS" +echo "DIR_FILE_COMMANDS=$DIR_FILE_COMMANDS" # Assuming you used https://github.com/actions/checkout, # the GITHUB_WORKSPACE variable corresponds to the following host dir: @@ -221,7 +224,7 @@ endGroup # 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" \ -v "$HOST_WORKSPACE_REPO:$PWD" -w "$PWD" \ - -v "$DIR_GITHUB_RUNNER_FILE_COMMANDS:$DIR_GITHUB_RUNNER_FILE_COMMANDS" \ + -v "$HOST_GITHUB_RUNNER_FILE_COMMANDS:$DIR_FILE_COMMANDS" \ "$COQ_IMAGE" /bin/bash --login -c " exec 2>&1 ; endGroup () { { init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; echo; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in *x*) set -x ;; esac; } ; startGroup () { { init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in *x*) set -x ;; esac; } # generated from helper.sh export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '; set -ex