Permit doc builds through workflow_dispatch (#497)

This PR adds a "workflow_dispatch" trigger to the build-docs workflow, so that we can trigger it directly (instead of, for example, having to find a trivial change to make to the source and rely on the resulting push to main to trigger the build).

.github/workflows/build-docs.yml

@@ -1,6 +1,7 @@
 name: Update gh-pages documentation for main branch
 
 on:
+  workflow_dispatch:
   push:
     branches:
     - main