Change WORKDIR in script, not relying on docker run -w by user (#4821)

* fix: #4459

* add exit code

* misc fix
This commit is contained in:
Kin Fai Tse 2023-11-05 12:29:52 +08:00 committed by GitHub
parent 35c3fa445c
commit d923938804
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -500,7 +500,9 @@ GetGitHubVars() {
fatal "Provided volume is not a directory!" fatal "Provided volume is not a directory!"
fi fi
info "Linting all files in mapped directory:[${DEFAULT_WORKSPACE}]" info "Linting all files in mapped directory:[${GITHUB_WORKSPACE}]"
pushd "${GITHUB_WORKSPACE}" >/dev/null || exit 1
# No need to touch or set the GITHUB_SHA # No need to touch or set the GITHUB_SHA
# No need to touch or set the GITHUB_EVENT_PATH # No need to touch or set the GITHUB_EVENT_PATH