Reverts part of commit 2539bd9 while keeping the intention of it:
To avoid duplicate CI runs when making and updating a PR.
Disabling `push` means we cannot push to a branch and see the CI results
directly without making a PR, which some of us use. There are many situations
where this is useful, and "[WIP]" PRs are not appropriate for all.
Disabling `pull_request` has a similar effect, removing duplicate CI.
It is known that `pull_request` _is_ needed when a third party sends a
PR (because it's not committed to the repo yet). But this is rare at the
moment, and there's a workaround: A committer can push the third party change
to a branch, triggering CI.
So re-enable `push`, disable `pull_request`, and we'll see if the latter
missing causes problems in practice. Won't know until we try it.
Note: This might be interim until `workflow_dispatch` is working better.
Perhaps that needs more configuration. Currently, `workflow_dispatch` is kind
of useless for CI tests, because it doesn't result in any CI indicator
associated with a commit or branch. Even the actions page doesn't show the
name of the branch, just a less-than-useful generic "CI" for these actions.
Signed-off-by: Jamie Lokier <jamie@shareable.org>
2fe2f23e70