Updates GitHub workflow for documentation build

[froschdesign]

No description provided.

[Ocramius]

Change looks harmless, but I don't understand it 🤔

[froschdesign]

The DOCS_DEPLOY_KEY is the legacy key and must be replaced:

# check values
remote_repo=""
if [ -n "${DEPLOY_TOKEN}" ]; then
    remote_repo_setup remote_repo "${DEPLOY_TOKEN}"
else
    if [ -n "${DOCS_DEPLOY_KEY}" ]; then
        remote_repo_setup_legacy remote_repo "${DOCS_DEPLOY_KEY}"
    else
        print_error "Neither DEPLOY_TOKEN nor DOCS_DEPLOY_KEY found; please provide one or the other in your workflow env"
        kill -s KILL $TOP_PID
    fi
fi

https://github.com/laminas/documentation-theme/blob/c9c95a899460735dc06ccff05ec47d1c4f95e8ba/github-actions/docs/entrypoint.sh#L64-L75

[Ocramius]

@froschdesign thanks! As a note for future changes, try putting this sort of reasoning in commits, when not too cumbersome 😁