chore: Enable docs workflow for main branch

Author: effigies

.github/workflows/docs-build-update.yml

@@ -3,10 +3,10 @@ name: Build & update docs
 
 on:
   push:
-    branches: [ 'doc/*', 'docs/*', master, "maint/*" ]
+    branches: [ 'doc/*', 'docs/*', master, main, "maint/*" ]
     tags: [ '*' ]
   pull_request:
-    branches: [ master, 'maint/*' ]
+    branches: [ master, main, 'maint/*' ]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
@@ -92,17 +92,17 @@ jobs:
         git push
 
     - name: Push "master" docs to gh-pages after a push to master (typically, a PR merge).
-      if: github.ref == 'refs/heads/master'
+      if: github.ref == 'refs/heads/master' || github.ref == 'refs/heads/main'
       run: |
-        if [[ "${CURBRANCH}" != "master" ]]; then
+        if [[ "${CURBRANCH}" != "master" -a "${CURBRANCH}" != "main" ]]; then
             echo "$CURBRANCH is not the default development branch"
             exit 1
         fi
         git checkout -b gh-pages origin/gh-pages
-        git rm -r master/ || true
+        git rm -r ${CURBRANCH}/ || true
         # It is fundamental that the directory does not exist at all.
-        rm -rf master
-        cp -r $HOME/docs/$CURBRANCH $PWD/master
-        git add master
-        git commit -am "docs(master): Update docs of development line" || true
+        rm -rf ${CURBRANCH}
+        cp -r $HOME/docs/$CURBRANCH $PWD/${CURBRANCH}
+        git add ${CURBRANCH}
+        git commit -am "docs(${CURBRANCH}): Update docs of development line" || true
         git push