When should docs build

[coretl]

3ecf702 made them run on every push and PR, with docs pushed to gh-pages on push. This has 3 issues:

1. Duplicate runs of docs builds for PRs from internal branches (can fix with if statement like in code.yaml)
2. Internal branch pushes will create new directories in gh-pages which are never deleted
3. Still can't see docs output from external repositories

I assume the change was made so you can see the docs output of a branch/PR. If so, we could fix in a few ways:

1. Keep this change, but add a new on: branch: delete workflow that removes the corresponding directory from gh-pages when a branch is deleted
2. Keep the change, but only publish to gh-pages on push to selected branches/tags, and always build the docs and upload as an artifact so reviewers can see it
3. Do both

[gilesknap]

I quite like just 1 so as not to use up (free) file space on out of date information.

[gilesknap]

This is fixed in b6282a2