GitHub: Add a GitHub Action to publish docs

Add a GitHub Action to publish docs automatically, whenever someone
pushes against the "main" branch.

Note we have chosen to implement the actual business logic of publishing docs
as part of the Makefile, rather than as part of the GitHub Action
directly. This means we only use the GitHub action to *automate* the
invocation of pre-existing business logic.

This allows us to run the exact same logic both locally and within a
GitHub Action. See here for interesting context:

https://news.ycombinator.com/item?id=33751533

Finally, ensure the docs-clean target actually depends on having created
the managed Python virtualenv, because it needs Sphinx-provided
commands.

Signed-off-by: Vangelis Koukis <[email protected]>

.github/workflows/docs-publish.yaml

@@ -0,0 +1,18 @@
+name: docs-publish
+
+on:
+  push:
+    branches:
+    - main
+  pull_request:
+    branches:
+    - main
+
+jobs:
+ docs-publish:
+   runs-on: ubuntu-latest
+   steps:
+   - name: checkout repo
+     uses: actions/checkout@main
+   - name: publish docs
+     run: make docs-publish

Makefile

@@ -31,8 +31,8 @@ docs: docs-build
 docs-build: venv
 	$(MAKE_VENV) -C docs html
 
-docs-clean:
-	make -C docs clean
+docs-clean: venv
+	$(MAKE_VENV) -C docs clean
 
 # Publish docs: Push to a specific branch at the same origin.
 # We have configured GitHub Pages to serve this branch,