Fixed exclusion of .doctrees

The reason was that the removal of files before syncing did not remove
directories starting with '.'.

Also, cleaned up the steps of setting up the worktree and syncing.

Signed-off-by: Andreas Maier <[email protected]>

.gh-pages-exclude

@@ -1,2 +1,5 @@
-.DS_Store
+# rsync exclude patterns for the documentation build. For details on the syntax,
+# see https://linuxize.com/post/how-to-exclude-files-and-directories-with-rsync/
+# or https://download.samba.org/pub/rsync/rsync.html.
+# Path names are relative to the 'docs_build' directory.
 .doctrees

.github/workflows/pages.yml

@@ -27,20 +27,24 @@ jobs:
       uses: actions/setup-python@v2
       with:
         python-version: '3.8'
-    - name: Setup development environment
+    - name: Set up development environment
       run: |
         make develop
     - name: Build documentation
       run: |
         ${{ env.doc_build_cmd }}
-    - name: Setup gh-pages worktree
+    - name: Set up gh-pages worktree
       run: |
          git worktree add gh-pages gh-pages
+         bash -c "cd gh-pages; git fetch"
     - name: Sync documentation to gh-pages worktree
       # The file .gh-pages-exclude defines files to be excluded from the sync
       run: |
-         bash -c "cd gh-pages; git fetch; rm -rf *"
-         rsync -a ${{ env.doc_build_dir }}/ gh-pages/ --exclude-from=.gh-pages-exclude
+         rm -rf gh-pages/*
+         rm -f gh-pages/.doctrees
+         rm -f gh-pages/.buildinfo
+         ls -al gh-pages
+         rsync -a --exclude-from=.gh-pages-exclude ${{ env.doc_build_dir }}/ gh-pages/
     - name: Commit changes in the gh-pages branch locally
       # The git config can specify any user name and email
       run: |