Run the main build on every push to main, not just root-file pushes (#2238)

main.yml filtered pushes with

  paths:
  - '*'
  - '!/docs/*'

GitHub's `*` does not cross a '/', so `'*'` matches only files at the repository
root. Any push touching just Dapper/, tests/ or another subdirectory failed the
filter and the build was skipped - silently, because a skipped workflow is not a
failure. Checking main:

  8becae8 (#2230)  4 root files  ran
  2ca8261 (#2223)  1 root file   ran
  6d48ef6 (#2228)  0 root files  skipped
  41d76c7 (#2225)  0 root files  skipped

So most merges to main never built at all. The second line never worked either:
path filters are repo-relative and take no leading slash, so '!/docs/*' matched
nothing - the docs exclusion it was written for was already being done, by
accident, by the '*' that excluded every subdirectory.

paths-ignore: 'docs/**' says what was meant: run for everything except a
docs-only change.

This matters more than it used to. release.yml takes its version from what a
green main run reports, so a main build that never runs means no version to tag
with - which is how this was noticed.

.github/workflows/main.yml

@@ -6,9 +6,11 @@ on:
   push:
     branches:
     - main
-    paths:
-    - '*'
-    - '!/docs/*' # Don't run workflow when files are only in the /docs directory
+    # paths-ignore, not paths: a `paths` list of '*' matches only root-level files, because
+    # GitHub's `*` does not cross a '/'. That silently skipped main builds for every push that
+    # touched only Dapper/, tests/ and so on - which is most of them
+    paths-ignore:
+    - 'docs/**' # don't run when only the docs site changed
 
 jobs:
   vm-job: