CI: Restore "push" events but disable "pull_request"

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>

.github/workflows/ci.yml

@@ -2,10 +2,9 @@ name: CI
 on:
   push:
     paths-ignore: ['doc/**', 'docs/**', '**/*.md', 'hive_integration/**']
-    branches:
-      - master
-  pull_request:
-    paths-ignore: ['doc/**', 'docs/**', '**/*.md', 'hive_integration/**']
+  # Disable `pull_request`.  Experimenting with using only `push` for PRs.
+  #pull_request:
+  #  paths-ignore: ['doc/**', 'docs/**', '**/*.md', 'hive_integration/**']
   workflow_dispatch:
 
 jobs: