Rework docs push

[will-cromar]

• Follow current GHA examples for deploying pages.
• Tweak logic for selecting subdir. As near as I can tell, every release commit was updating master's docs:

  xla/.circleci/doc_push.sh

  Lines 22 to 26 in b834e49

  	if [[ "$BRANCH_NAME" == release/* ]]; then
  	SUBDIR_NAME=$BRANCH_NAME
  	else
  	SUBDIR_NAME="master"
  	fi

• Use token from GHA instead of bot account. Nope, org policy forbids us from getting a GHA token with write access
• Run docs build for every event, but only publish for pushes. You can check what the generated docs will look like in the github-pages artifact (releases/$PR_NUMBER/merge)

[will-cromar]

The nested job 'deploy' is requesting 'pages: write, id-token: write', but is only allowed 'pages: none, id-token: none'.

Hmmm, there may be a repository setting we need to change.