More documentation auto-building (#478)

* Make Git configuration global; suppress Git output about initial branch name

* Use full form of the name for clarity

.github/workflows/build-docs.yml

@@ -31,8 +31,8 @@ jobs:
         python -m pip install .[docs]
     - name: Configure Git
       run: |
-        git config user.name "Documentation Bot"
-        git config user.email "<>"
+        git config --global user.name "Documentation Bot"
+        git config --global user.email "<>"
     - name: Build documentation and deploy to gh-pages
       run: |
         python scripts/update_docs.py --token ${{ secrets.GITHUB_TOKEN }} ${{ github.ref }}

scripts/update_docs.py

@@ -132,7 +132,9 @@ def clone_branch(repo, branch, target_directory, name):
     clone_directory = os.path.join(target_directory, name)
     os.mkdir(clone_directory)
     with current_directory(clone_directory):
-        run_git("init")
+        # Specify a branch name to silence Git's output about the master->main
+        # change.
+        run_git("init", "--initial-branch=main")
         run_git("remote", "add", "origin", repo)
         run_git("fetch", "--no-tags", "--prune", "--depth=1", "origin", branch)
         run_git("checkout", branch)