Skip to content

Commit

Permalink
Update entrypoint.sh
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross authored May 10, 2024
1 parent b661553 commit 45881c7
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions entrypoint.sh
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,9 @@ if test -z "$INPUT_CUSTOM_SCRIPT_EXPANDED"; then
exit 1
fi

# set permissions for GitHub Actions runner command files
sudo chmod -R a=u "$DIR_GITHUB_RUNNER_FILE_COMMANDS"

startGroup "Pull docker image"

echo COQ_IMAGE="$COQ_IMAGE"
Expand Down

0 comments on commit 45881c7

Please sign in to comment.